| 研究概要 |
本研究では,定理の証明でしばしば用いられる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の年会にて招待講演予定.
の実績を上げることができた.
|
