An Automated Theorem Finding System for General-purpose and Its Applications

• Project/Area Number: 19700127
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Single-year Grants
• Research Field: Intelligent informatics
• Research Institution: Saitama University
• Principal Investigator: GOTO Yuichi Saitama University, 大学院理工学研究科, 助教 (70400801)
• Project Period (FY): 2007 – 2008
• Project Status: Completed (Fiscal Year 2008)
• Budget Amount: ¥2,780,000 (Direct Cost: ¥2,300,000、Indirect Cost: ¥480,000); Fiscal Year 2008: ¥2,080,000 (Direct Cost: ¥1,600,000、Indirect Cost: ¥480,000); Fiscal Year 2007: ¥700,000 (Direct Cost: ¥700,000)
• Keywords: 情報システム / 知識工学 / 自動発見

Research Abstract

自動定理発見問題に対して帰結演算による自動定理発見法が提案されたがいまだ実現されていない.本研究では,帰結演算による自動定理発見法において中心的役割を果たす汎用自動前向き帰結演算システムを実装し,公理的集合論において帰結演算による自動定理発見を試みるのが最終目的である.支援期間内には,論理式を構成する語彙,論理式の構成規則,公理,そして,推論規則を入力として自由に与えられるようにした汎用前向き推論エンジンFreeEnCalの開発を行った.また,開発したFreeEnCalの処理アルゴリズムを見直し処理の高速化を行った.

Research Products

• [Journal Article] A Deontic Relevant Logic Approach to Reasoning about Actions in Computing Anticipatory Systems (2008)
  • Author(s): Natsumi Kitajima, Shisuke Nara, Yuichi Goto, and Jingde Cheng
  • Journal Title: International Journal of Computing Anticipatory Systems Vol. 20 Pages: 177-190
  • Peer Reviewed
• [Journal Article] Anticipatory Reasoning about Mobile Objects in Anticipatory Reasoning-Reacting Systems (2008)
  • Author(s): Jingde Cheng, Yuichi Goto, and Natsumi Kitajima
  • Journal Title: "Computing Anticipatory Systems: CASYS 2007 - Eighth International Conference, Liege, Belgium, 6-11 August 2007"(D. M. Dubois (Ed.)), AIP Conference Proceedings(American Institute of Physics) Vol. 1051 Pages: 244-254
  • Peer Reviewed
• [Journal Article] A Fast Duplication Checking Algorithm for Forward Reasoning Engines (2008)
  • Author(s): Takahiro Koh, Yuichi Goto, and Jingde Cheng
  • Journal Title: "Knowledge-Based Intelligent Information and Engineering Systems, 12th International Conference, KES 2008, Zagreb, Croatia, September 3-5, 2008, Proceedings" (I. Lovrek, R. J. Howlett, and L. C. Jain (Eds.)), Lecture Notes in Artificial Intelligence (Subs Vol. 5178 Pages: 499-507
  • Peer Reviewed
• [Journal Article] A General Forward Reasoning Algorithm for Various Logic Systems with Different Formalizations (2008)
  • Author(s): Yuichi Goto, Takahiro Koh, and Jingde Cheng
  • Journal Title: "Knowledge-Based Intelligent Information and Engineering Systems, 12th International Conference, KES 2008, Zagreb, Croatia, September 3-5, 2008, Proceedings, Part II"(I. Lovrek, R. J. Howlett, and L. C. Jain (Eds.)), Lecture Notes in Artificial Intelligen Vol. 5178 Pages: 526-535
  • Peer Reviewed
• [Journal Article] A Fast Duplication Checking algorithm for Forward Reasoning Engines (2008)
  • Author(s): T. Koh, Y.Goto, J.Cheng
  • Journal Title: Lecture Notes in Artificial Intelligence 5178 Pages: 499-507
  • Peer Reviewed
• [Journal Article] A General Forward Reasoning algorithm for Various Logic Systems with Different Formalizations (2008)
  • Author(s): Y. Goto, T. Koh, J. Cheng
  • Journal Title: Lecture Notes in Artificial Intelligence 5178 Pages: 526-535
  • Peer Reviewed
• [Journal Article] Anticipatory Reasoning about Mobile Objects in Anticipatory Reasoning-Reacting Systems (2008)
  • Author(s): J. Cheng, Y. Goto, N. Kitajima
  • Journal Title: AIP Conference Proceedings 1051 Pages: 244-254
  • Peer Reviewed
• [Journal Article] A Deontic Relevant Logic Approach to Reasoning about Actions in Computing Anticipatory System (2008)
  • Author(s): N. Kitajima, Y. Goto, J. Cheng
  • Journal Title: International Journal of Computing Anticipatory Systems 20 Pages: 177-190
  • Peer Reviewed
• [Journal Article] FreeEnCal: A Forward Reasoning Engine with General-Purpose (2007)
  • Author(s): Jingde Cheng, Shinsuke Nara, and Yuichi Goto
  • Journal Title: "Knowledge-Based Intelligent Information and Engineering Systems, 11th International Conference, KES 2007, XVII Italian Workshop on Neural Networks, Vietri sul Mare, Italy, September 12-14, 2007, Proceedings, Part II"(B. Apolloni, R. J. Howlett, and L. C. Vol. 4693 Pages: 444-452
  • Peer Reviewed
• [Journal Article] A Cooperative Grid Computing Approach to Automated Theorem Finding and Automated Problem Proposing (2007)
  • Author(s): Jingde Cheng, Yuichi Goto, Shinsuke Nara, and Takahiro Koh
  • Journal Title: "Knowledge-Based Intelligent Information and Engineering Systems, 11th International Conference, KES 2007, XVII Italian Workshop on Neural Networks, Vietri sul Mare, Italy, September 12-14, 2007, Proceedings, Part II"(B. Apolloni, R. J. Howlett, and L. C. Vol. 4693 Pages: 840-851
  • Peer Reviewed
• [Journal Article] EPLAS: An Epistemic Programming Language for All Scientists (2007)
  • Author(s): Isao Takahashi, Shinsuke Nara, Yuichi Goto, and Jingde Cheng
  • Journal Title: "Computational Science - ICCS 2007: 7th International Conference, Beijing, China, May 27-30, 2007, Proceedings, Part I"(Y. Shi (Eds.)), Lecture Notes in Computer Science(Springer-Verlag) Vol. 4487 Pages: 406-413
  • Peer Reviewed
• [Journal Article] EPLAS: An Epistemic Programming Language for All Scientists (2007)
  • Author(s): Isao TAKAHASHI, Shinsuke NARA, Yuichi GOTO, and Jingde CHENG
  • Journal Title: Lecture Notes in Computer Science 4487 Pages: 406-413
  • Peer Reviewed
• [Journal Article] FreeEnCal: A Forward Reasoning Engine with General-Purpose (2007)
  • Author(s): Jingde CHENG, Shinsuke NARA, and Yuichi GOTO
  • Journal Title: Lecture Notes in Computer Science 4693 Pages: 444-452
  • Peer Reviewed
• [Journal Article] A Cooperative Grid Computing Approach to Automated Theorem Finding and Automated Problem Proposing (2007)
  • Author(s): Jingde CHENG, Yuichi GOTO, Shinsuke NARA, and Takahiro KOH
  • Journal Title: Lecture Notes in Computer Science 4693 Pages: 840-851
  • Peer Reviewed
• [Presentation] Fast Qualitative Reasoning about Actions for Computing Anticipatory Systems (2008)
  • Author(s): Natsumi Kitajima, Yuichi Goto, and Jingde Cheng
  • Organizer: Proceedings of the 3rd International Conference on Availability, Reliability and Security (ARES '08)(IEEE Computer Society Press), pp. 171-178
  • Place of Presentation: Barcelona, Spain
  • Year and Date: 2008-03-04
• [Presentation] Fast Qualitative Reasoning about Actions for Computing Antic ipatory Systems (2008)
  • Author(s): Natsumi KITAJIMA, Yuichi GOTO, and Jingde CHENG
  • Organizer: The 3rd International Conference on Availability, Reliability and Security
  • Place of Presentation: Barcelona, Spain