1999 Fiscal Year Annual Research Report
| Project/Area Number |
11780236
|
|---|
| Research Institution | Hiroshima City University |
|---|
Principal Investigator |
新井 紀子 広島市立大学, 情報科学部, 助手 (40264931)
|
|---|
| Keywords | 証明論 / 自動証明 / 計算の複雑さ / 計算量 / ロジック |
|---|
| Research Abstract |
本研究では,定理の証明でしばしば用いられるbrute-force-inductionとwithout-loss-of-generalityという二つの論理的考察方法に着目した.これを命題論理のシーケント計算上に実現することにより,従来型の自動証明機を越えて,知的な推論を一部行なうことができるような命題論理の自動証明機を開発すること,そして,この体系を理論的に分析することにより,この体系の限界を探ることを目的としていた.本年度の成果として,
1.(理論的分析)symmetry法をレゾリューション上で展開した時の理論的限界を示し,これを,"Local Symmetries in Propositional Logic"として論文とした.国際会議Tableaux and related methodにて招待講演予定.
2.(実験開発)Simple Combinatorial Reasoningを自動証明機としてC上で実現することに成功した.鳩の巣原理など初等組合せ論の問題に対して,この自動証明機はすでに提案されているDavis-Putnam法やその改良版に比べ,圧倒的に早く証明をすることができることを実験により示した.Association of Symbolic Logicの年会にて招待講演予定.
の実績を上げることができた.
|
-
[Publications] Noriko Arai,Alasdair Urquhart: "Local symmetries in propositional Logic"Lecture Notes in Artificial Intelligence. (予定).
-
[Publications] Noriko Arai: "Relative efficiency of propositional proof systems:resolution vs.cut-free LK"Annals of Pure and Applied Logic. (予定).
-
[Publications] 新井紀子,枡川竜治: "知的自動証明機の提案と実装"京都大学数理学研究所講演録. (予定).
