Development of Multi-Context Reasoning Infrastructural Systems for Algebraic Software

• Project/Area Number: 19500020
• 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 Hokkaido University, 大学院・情報科学研究科, 教授 (50133707)
• Project Period (FY): 2007 – 2009
• Project Status: Completed (Fiscal Year 2009)
• Budget Amount: ¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000); Fiscal Year 2009: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2008: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2007: ¥2,470,000 (Direct Cost: ¥1,900,000、Indirect Cost: ¥570,000)
• Keywords: ソフトウェア学 / システム工学 / ディペンダブル・コンピューティング / 人工知能 / 項書換え系 / 完備化手続き / 国際情報交換 / オーストリア / 定理自動証明 / 停止性

Research Abstract

In the field of algebraic computer software called the term rewriting systems, this project has successfully developed a new infrastructural reasoning system which solves a lot of problems efficiently. The problems include the completion problems for transforming programs into those which always terminate and output the unique solution. Also included is the automated inductive theorem proving for proving crucial properties to be satisfied by programs. The key technology is the multi-context reasoning which allows very efficient simulation of parallel execution of multiple processes using the special data structure called nodes and heuristic search.

Research Products

• [Journal Article] Multi-context rewriting induction with termination checkers (Special Section on Formal Approach) (2010)
  • Author(s): Haruhiko Sato, Masahito Kurihara
  • Journal Title: IEICE Transactions on Information and Systems Vol. E93-D, No. 5(採録決定)
  • Peer Reviewed
• [Journal Article] Hardness measures for gridworld bench-marks and performance analysis of realtime heuristic search algorithms (2010)
  • Author(s): Masataka Mizusawa, Masahito Kurihara
  • Journal Title: Journal of Heuristics Vol. 16 Pages: 23-36
  • Peer Reviewed
• [Journal Article] Hardness measures for gridworld benchmarks and performance analysis of real-time heuristic search algorithms (2010)
  • Author(s): Masataka Mizusawa, Masahito Kurihara
  • Journal Title: Journal of Heuristics 16 Pages: 23-36
  • 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(Special Section on Formal Approach) E93-D(未定(採択決定・編集中)) Pages: 1-1
  • NAID: 10026815209
• [Journal Article] A Tool for Visualizing the Behavior of Fuzzy Constraint Satisfaction Solvers (2010)
  • Author(s): Takuto Yanagida, Masahito Kurihara, Hidetoshi Nonaka
  • Journal Title: Journal of Advanced Computational Intelligence & Intelligent Informatics 14(未定(採択決定・編集中)) Pages: 1-1
• [Journal Article] Constraint-based multi-completion procedures for term rewriting systems (Special Section on Foundation of Computer Science) (2009)
  • Author(s): Haruhiko Sato, Masahito Kurihara, Sarah Winkler, Aart Middeldorp
  • Journal Title: IEICE Transactions on Information and Systems Vol. E92-D, No. 2 Pages: 220-234
  • Peer Reviewed
• [Journal Article] Constraint-Based Multi-Completion Procedures for Term Rewriting Systems (2009)
  • Author(s): Haruhiko Sato, Masahito Kurihara, Sarah Winkler, Aart Middeldorp
  • Journal Title: IEICE Transactions on Information and Systems (Special Section on Foundation of Computer Science) E92-D Pages: 220-234
  • NAID: 10026807461
  • Peer Reviewed
• [Journal Article] Computational Dialectics Based on Specialization and Generalization-A New Reasoning Method for Conflict Resolution (2009)
  • Author(s): Hiroyuki Kido and Masahito Kurihara
  • Journal Title: Lecture Notes in Artificial Intelligence 5447 Pages: 228-241
  • Peer Reviewed
• [Journal Article] Hardness measures for gridworld benchmarks and performance-analysis of real-time heuristic search algorithms (2008)
  • Author(s): Masataka Mizusawa and Masahito Kurihara
  • Journal Title: Journal of-Heuristics 2008(Online) Pages: 1-14
  • Peer Reviewed
• [Presentation] Optimizing mkbTT (2010)
  • Author(s): Sarah Winkler, Haruhiko Sato, Aart Middeldorp, Masahito Kurihara
  • Organizer: International Conference on Rewriting Techniques and Applications
  • Place of Presentation: エジンバラ大学 (英国エジンバラ市)
  • Year and Date: 2010-07-11
• [Presentation] Design and Implementation of Multi-Context Rewriting Induction (2010)
  • Author(s): Haruhiko Sato, Masahito Kurihara
  • Organizer: IAENG International MultiConference of Engineers and Computer Scientists
  • Place of Presentation: ロイヤルガーデンホテル (香港)
  • Year and Date: 2010-03-17
• [Presentation] Design and Implementation of Multi-Context Rewriting Induction (2010)
  • Author(s): Haruhiko Sato, Masahito Kurihara
  • Organizer: International MultiConference of Engineers and Computer Scientists
  • Place of Presentation: ロイヤルガーデンホテル、香港(中国)
  • Year and Date: 2010-03-17
• [Presentation] Multi-Context Rewriting Induction (2010)
  • Author(s): Masahito Kurihara, Haruhiko Sato
  • Organizer: International Symposium on Global COE Program of Center for Next-Generation Information Technology Based on Knowledge Discovery and Knowledge Federation
  • Place of Presentation: 北海道大学学術交流会館 (札幌)
  • Year and Date: 2010-01-19
• [Presentation] Multi-Context Rewriting Induction (2010)
  • Author(s): Masahito Kurihara, Haruhiko Sato
  • Organizer: 3rd International Symposium on Global COE Program of Center for Next-Generation Information Technology Based on Knowledge Discovery and Knowledge Federation
  • Place of Presentation: 北海道大学学術交流会館、札幌
  • Year and Date: 2010-01-19
• [Presentation] Userfriendly GUI in software model checking (2009)
  • Author(s): Shoichi Yokoyama, Haruhiko Sato, Masahito Kurihara
  • Organizer: IEEE International Conference on Systems, Man, and Cybernetics
  • Place of Presentation: ハイアット・リージェンシーホテル (米国サンアントニオ市)
  • Year and Date: 2009-10-12
• [Presentation] User-friendly GUI in software model checking (2009)
  • Author(s): Shoichi Yokoyama, Haruhiko Sato, Masahito Kurihara
  • Organizer: 2009 IEEE International Conference on Systems, Man, and Cybernetics
  • Place of Presentation: ハイアット・リージェンシーホテル、サンアントニオ(米国)
  • Year and Date: 2009-10-12
• [Presentation] Implementation and performance evaluation of multi-completion with termination checking (2008)
  • Author(s): Haruhiko Sato, Masahito Kurihara
  • Organizer: IEEE International Conference on Systems, Man, and Cybernetics
  • Place of Presentation: サンテック国際会議展示場 (シンガポール)
  • Year and Date: 2008-10-12
• [Presentation] Multicompletion with termination tools (2008)
  • Author(s): Haruhiko Sato, Sarah Winkler, Masahito Kurihara, Aart Middeldorp
  • Organizer: International Joint Conference on Automated Reasoning
  • Place of Presentation: メキュアホテル (豪州シドニー市)
  • Year and Date: 2008-08-10
• [Presentation] Design and Implementation of Multicompletion procedures with termination checking (2008)
  • Author(s): Haruhiko Sato, Masahito Kurihara
  • Organizer: International Conference on Theoretical and Mathematical Foundations of Computer Science
  • Place of Presentation: インペリアル・スワンホテル (米国オーランド市)
  • Year and Date: 2008-07-07
• [Presentation] Multi-completion procedures for term rewriting systems with modern termination checking (2008)
  • Author(s): Haruhiko Sato, Masahito Kurihara
  • Organizer: International Conference on Computing, Communications and Control
  • Place of Presentation: ローゼンセンター (米国オーランド市)
  • Year and Date: 2008-06-29
• [Presentation] Multi-completion procedures for term rewriting systems based on constraint system, Proc (2008)
  • Author(s): Haruhiko Sato, Masahito Kurihara
  • Organizer: International Conference on Information Technology and Appli-cations
  • Place of Presentation: ヒルトンホテル (豪州ケアンズ市)
  • Year and Date: 2008-06-23
• [Presentation] MKBOOL : A multi-completion system for boolean constrained reduction orders (2008)
  • Author(s): Haruhiko Sato, Masahito Kurihara
  • Organizer: IAENG International MultiConference of Engineers and Computer Scientists
  • Place of Presentation: リーガル・カオルーンホテル (香港)
  • Year and Date: 2008-03-19
• [Presentation] Multi-completion with termination tools (2008)
  • Author(s): Haruhiko Sato, Sarah Winkler, Masahito Kurihara and Aart Middeldorp
  • Organizer: 4th International Joint Conference on Automated Reasoning
  • Place of Presentation: Mecure Sydney Hotel (Sydney)
• [Presentation] Implementation and performance evaluation of multi-completion with termination checking (2008)
  • Author(s): Haruhiko Sato and Masahito Kurihara
  • Organizer: 2008 IEEE International Conference on Systems, Man, and Cybernetics
  • Place of Presentation: Suntec Singapore Convention Exhibition Centre (Singapore)
• [Presentation] Design and Implementation of Multi-completion procedures with termination checking (2008)
  • Author(s): Haruhiko Sato and Masahito Kurihara
  • Organizer: International Conference on Theoretical and Mathematical Foundations of Computer Science
  • Place of Presentation: Imperial Swan Hotel & Suites (Orlando)
• [Presentation] Multi-completion procedures for term rewriting systems with modern termination checking (2008)
  • Author(s): Haruhiko Sato and Masahito Kurihara
  • Organizer: International Conference on Computing, Communications and Control
  • Place of Presentation: Rosen Centre Hotel (Orlando)
• [Presentation] Multi-completion procedures for term rewriting systems based on constraint system (2008)
  • Author(s): Haruhiko Sato and Masahito Kurihara
  • Organizer: International Conference on Information Technology and Applications
  • Place of Presentation: Hilton Cairns Hotel (Cairns)
• [Presentation] MKBOOL: A multi-completion system for boolean constrained reduction orders (2008)
  • Author(s): Haruhiko Sato and Masahito Kurihara
  • Organizer: International MultiConference of Engineers and Computer Scientists 2008(IMECS 2008)
  • Place of Presentation: リーガル・カオルーンホテル(香港)
• [Presentation] Searching for successful reduction orders in equational multi-completion with boolean constraints (2008)
  • Author(s): Masahito Kurihara and Haruhiko Sato
  • Organizer: International Symposium on Global COE Program of Center for Next-Generation Information Technology based on Knowledge Discovery and Knowledge Federation(GCOE-NGIT 2008)
  • Place of Presentation: 北海道大学(札幌)
• [Presentation] 依存対法を用いた項書換え系多重完備化手続き (2007)
  • Author(s): 佐藤 晴彦, 栗原 正仁
  • Organizer: 日本ソフトウェア科学会第24回大会
  • Place of Presentation: 奈良先端科学技術大学院大学(奈良)
• [Presentation] 依存対法を用いた項書換え系多重完備化手続き (2007)
  • Author(s): 佐藤 晴彦, 栗原 正仁
  • Organizer: 電子情報通信学会ソフトウェアサイエンス研究会
  • Place of Presentation: 北海道大学(札幌)