証明支援システムxpe(<特集>自動推論 : 演繹, 帰納, モデル検査/生成, 仮説推論アブダクション, 論理プログラム, プランニング, 時相論理, etc.)
スポンサーリンク
概要
- 論文の詳細を見る
本稿では,証明支援システムとしてのxpeについて説明する.本システムは数理論理学における形式的証明を支援するシステムである.xpeは元々はTEXの証明図マクロproof.styと互換性を持つ証明図作成ソフトであった.TEXのコマンドを解釈・表示し,必要に応じて証明図に論理式の挿入を行うことができる.そして,xpeをユーザーインターフェースとし,xpeから定理自動証明プログラムを呼び出すことで,全体として新しい形の証明支援システムを提供する.xpeを用いることにより証明図の可読性や再利用性が極めて高くなる.xpeはインタラクティブな操作性を持つので,証明途中の証明図を入力し未完成な部分を定理自動証明プログラムにかけることで全体の証明図を得ることも可能である.このように,xpeは定理自動証明を越えた証明支援システムを提供する.
- 2002-05-17