Mathematical Logic · Section 4

反駁手続きから空節 □ への旅

コンピュータにとって「ある論理式が常に真であること」を直接証明するのは難しい。 そこで 否定をとって矛盾を見つける「反駁」のアプローチをとります。 その先には ∃ を消し、∀ と ∧ を削ぎ落とし、最終的に [ [...], [...] ] という配列構造（節集合）と 空節 □ が待っています。