Scalable Parallel Implementation and Application of Multi-ContextReasoning Systems for Algebraic Software

• Project/Area Number: 22500022
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: Hokkaido University
• Principal Investigator: KURIHARA Masahito 北海道大学, 大学院・情報科学研究科, 教授 (50133707)
• Co-Investigator(Renkei-kenkyūsha): SATO Haruhiko 北海道大学, 大学院・情報科学研究科, 助教 (30543178)
• Project Period (FY): 2010 – 2012
• Project Status: Completed (Fiscal Year 2012)
• Budget Amount: ¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000); Fiscal Year 2012: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000); Fiscal Year 2011: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000); Fiscal Year 2010: ¥2,990,000 (Direct Cost: ¥2,300,000、Indirect Cost: ¥690,000)
• Keywords: 項書換え系 / 並列化 / 多重文脈型推論 / 人工知能 / ソフトウェア / 代数 / 項書換えシステム / 並列プログラミング / 多重文脈推論 / 停止性検証 / ソフトウェア学 / 代数学

Research Abstract

In order to extend the multi-context reasoning systems to physically parallel executable frameworks, the processes for termination verification including creation and update of equations and rewrite rules and, in particular, the implementation of the determination of system termination (success) among the processes have been considered and by using a parallel programming language Erlang, a scalable, parallel implementation scheme on parallel computers has been developed to give the systems more power. Also, the systems have been applied to problems such as inductive theorem proving to see their improved usability.

Research Products

• [Journal Article] Multi-Completion with Termination Tools (2013)
  • Author(s): Sarah Winkler, Haruhiko Sato, Aart Middeldorp, Masahito Kurihara
  • Journal Title: Journal of Automated Reasoning Volume: Vol. 50, No.3 Pages: 317-354
  • NAID: 120005228268
  • Peer Reviewed
• [Journal Article] Multi-context rewriting induction with termination checkers (2010)
  • Author(s): Haruhiko Sato, Masahito Kurihara
  • Journal Title: IEICE Transactions on Information and Systems Volume: Vol.E93-D, No.5 Pages: 942-952
  • NAID: 10026815209
  • Peer Reviewed
• [Presentation] Parallelization of termination checker for term rewriting system (2012)
  • Author(s): Rui Ding, Haruhiko Sato, Masahito Kurihara
  • Organizer: The 2012 IEEE International Conference on Systems, Man, and Cybernetics, 1824-1829
  • Place of Presentation: Seoul(韓国)COEX 国際会議場
  • Year and Date: 2012-10-15
• [Presentation] Parallelization of termination checker of term rewriting systems (2012)
  • Author(s): Rui Ding, Haruhiko Sato, Masahito Kurihara
  • Organizer: The International MultiConference of Engineers and Computer Scientists 2012
  • Place of Presentation: 香港(中国)ロイヤルガーデンホテル
  • Year and Date: 2012-03-15
• [Presentation] Parallelization of Termination Checker of Term Rewriting Systems (2012)
  • Author(s): Rui Ding, Haruhiko Sato, Masahito Kurihara
  • Organizer: International MultiConference of Engineers and Computer Scientists
  • Place of Presentation: The Royal Garden Hotel(香港)
  • Year and Date: 2012-03-14
• [Presentation] Parallelization of termination checker using dependency pair method (2012)
  • Author(s): 丁睿, 佐藤晴彦, 栗原正仁
  • Organizer: 情報処理学会第74回全国大会
  • Place of Presentation: 名古屋工業大学(名古屋)
  • Year and Date: 2012-03-08
• [Presentation] Multi-context rewriting induction with termination checkers (2012)
  • Author(s): Haruhiko Sato, Masahito Kurihara
  • Organizer: The 5th International Symposium on Global COE Program of Center for Next-GenerationInformation Technology Based on Knowledge Discovery and Knowledge Federation
  • Place of Presentation: 札幌 ,北海道大学
  • Year and Date: 2012-01-16
• [Presentation] Comment-based keyword programming (2011)
  • Author(s): Yusuke Sakamoto, Haruhiko Sato, Satoshi Oyama, Masahito Kurihara
  • Organizer: International MultiConference of Engineers and Computer Scientists
  • Place of Presentation: ロイヤルガーデンホテル,香港,中国
  • Year and Date: 2011-03-17
• [Presentation] Optimizing mkbTT (2010)
  • Author(s): Sarah Winkler, Haruhiko Sato, Aart Middeldorp, Masahito Kurihara
  • Organizer: The 21st International Conference on Rewriting Techniques and Applications
  • Place of Presentation: Edinburgh(英国)エジンバラ大学
  • Year and Date: 2010-07-12
• [Presentation] Optimizing mkbTT (2010)
  • Author(s): Sarah Winkler, Haruhiko Sato, Aart Middeldorp, Masahito Kurihara
  • Organizer: 21st International Conference on Rewriting Techniques and Applications
  • Place of Presentation: エジンバラ大学,エジンバラ,英国
  • Year and Date: 2010-07-11
• [Presentation] Parallelization of Termination Checker for Term Rewriting System
  • Author(s): Masahito Kurihara
  • Organizer: IEEE International Conference on Systems, Man, and Cybernetics
  • Place of Presentation: COEX会議場（ソウル）
• [Remarks]
  • URL: http://kussharo.complex.eng.hokudai.ac.jp/file/satoh.pdf