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

2012 Fiscal Year Final Research Report

• 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
• 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
  • 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
  • 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] 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] 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
• [Remarks]
  • URL: http://kussharo.complex.eng.hokudai.ac.jp/file/satoh.pdf