論理的推論と定理証明

論理的推論と定理証明は、形式論理を用いて知識を表現すること、および前提の集合から必然的に導かれる結論を推論する演繹の自動化に関わる分野である。

Definition

定理証明とは、通常、論理式を健全な推論規則で操作し、目標が導出されるか矛盾に達するまで繰り返すことで、ある論理式が一連の公理から導かれるかどうかを自動的に導出することである。

Scope

このトピックでは、命題論理と一階述語論理における推論、およびそれを自動化するアルゴリズムについて扱う。具体的には、命題論理における真理値表とDPLLに基づく充足可能性検査、一階述語論理における単一化と導出原理、前方連鎖と後方連鎖、そして論理プログラミングの基礎が含まれる。また、推論手続きの健全性、完全性、決定可能性についても論じる。不確実性やデフォルトを許容する推論については、不確実性下の推論および非単調推論に関する関連トピックで扱われる。

Core questions

• 結論がある前提の集合によって含意されるとはどういう意味か、そして含意は機械的にどのように検証されるのか。
• 単一化を伴う導出原理は、一階述語論理に対する単一の完全な推論規則をどのように提供するのか。
• 前方連鎖と後方連鎖は、推論戦略としてどのように異なるのか。
• 一階述語論理の妥当性が半決定可能であるという事実を考慮すると、自動推論の限界は何か。

Key concepts

• 命題論理と一階述語論理
• 含意と妥当性
• 単一化
• 導出と反駁
• DPLLとSATソルビング
• 前方連鎖と後方連鎖
• Horn節と論理プログラミング
• 健全性と完全性

Key theories

導出原理

Robinsonの導出原理は、節に対する単一の推論規則であり、単一化と組み合わせることで一階述語論理に対して反駁完全である。すなわち、任意の充足不能な節の集合は、空節を導出することによって充足不能であることが示される。

DPLLと命題充足可能性

Davis-Putnam手続きとそのDPLL改良版は、単位伝播と純粋リテラル消去を伴う体系的な場合分けによって命題充足可能性を決定し、現代のSATソルバーの基礎を形成している。

論理プログラミングと後方連鎖

一階述語論理をHorn節に制限し、目標を後方連鎖で解決することで論理プログラミングが実現される。ここでは計算が証明探索となり、推論手法とプログラミングパラダイムの両方を提供する。

Clinical relevance

自動定理証明とSAT/SMTソルビングは、ハードウェアおよびソフトウェアの検証、プログラム解析、計画、数学において利用されている。一方、Prologのような論理プログラミング言語は、後方連鎖推論をデータベース、構文解析、ルールベースシステムに応用している。

History

Gilmore、Davis、Putnam（1960年）による初期の証明手続きは、命題論理と量化推論を自動化し、Robinsonの導出原理（1965年）は、一階述語論理の推論を単一の規則に統合した。1970年代には、導出原理が論理プログラミングとPrologへと洗練され、SATおよびSMTソルビングは後に主要な実用技術へと発展した。

Key figures

• John Alan Robinson
• Martin Davis
• Hilary Putnam
• Robert Kowalski
• Alan Robinson

Seminal works

• robinson1965
• davis1960
• kowalski1979

Frequently asked questions

導出原理とは何か？

導出とは、相補的なリテラルを含む2つの節を受け取り、残りの部分を結合した新しい節を生成する単一の推論規則である。単一化と組み合わせて繰り返し適用することで、一階述語論理の節の集合が充足不能であることを示すことができ、これは反駁による定理証明の基礎となる。

自動定理証明は終了が保証されているか？

命題論理の場合、妥当性は決定可能であるため、手続きは終了する。完全な一階述語論理の場合、妥当性は半決定可能に過ぎない。完全な証明器は、任意の妥当な論理式を最終的に確認するが、妥当でない論理式に対しては永遠に実行され続ける可能性があり、したがって一般的に終了は保証されない。