反駁手続き

コンピュータにとって「ある論理式が常に正しい（妥当である）」ことを正面から証明するのは、無限のモデルを尽くす作業になり困難です。

そこで 「証明したい式の否定をとり、それが矛盾する（決して真にならない）こと」を探すアプローチをとります。これを 反駁（Refutation）と呼びます。ここから先のアプリの目的は、正しいことを証明することからエラー（矛盾）を見つけることに切り替わります。

反駁の最初の一歩は、式全体に否定 ¬ を付け、ド・モルガンの法則と量化子の入れ替えで否定をリテラル（P や ¬Q）まで内側に押し込むことです。 下のシミュレーターで動かしてみてください。