Loading article…
凝縮分離（ルールD）は、2つの形式的な論理命題が与えられた場合に、最も一般的な結論を見つける方法です。これは、1950年代にアイルランドの論理学者カリュー・メレディスによって開発され、ルカシェヴィチの研究に触発されました。[ 1 ]
分離の規則（しばしばモーダス・ポネンスと呼ばれる）は 次のように述べている。「暗示する、そして与えられた推論する。
要約すると、さらに一歩進んでこう述べている。 「暗示する、そしてユニファイアを使用するそして作るそして同じ条件であれば、標準的な分離ルールを適用してください。」
置換Aを 適用すると生産する、置換Bを適用すると生産するは、そして。
様々な統一子によって、自由変数の数が異なる式が生成される場合があります。可能な統一式の中には、他の式の置換インスタンスとなるものがあります。ある式が別の式の置換インスタンスである場合（単なる変数名の変更ではなく）、その別の式は「より一般的な式」と呼ばれます。
最も一般的な統一子が簡約分離で使用される場合、論理的な結果は、与えられた2番目の式を用いた推論において導き出せる最も一般的な結論となります。得られる推論はすべて最も一般的な推論の置換例であるため、実際には最も一般的な統一子以外のものは決して使用されません。
古典命題論理のような一部の論理体系は、「D完全性」特性を持つ定義公理の集合を持っています。公理の集合がD完全であれば、その体系の有効な定理はすべて、変数名の変更を除いて、その置換インスタンスも含めて、縮約分離のみによって生成できます。たとえば、これはD完全系の定理であり、凝縮分離法は、その定理だけでなく、その置換インスタンスも証明できる。より長い証明を用いることで。なお、「D完全性」はシステムの公理的基底の性質であり、論理システム自体の固有の性質ではないことに注意されたい。[ 2 ]
J.A. カルマンは、一様置換（変数のすべてのインスタンスが同じ内容に置き換えられる）とモーダス・ポネンスのステップのシーケンスによって生成できる結論は、凝縮分離のみによって生成できるか、または凝縮分離のみによって生成できるものの置換インスタンスであることを証明した。[ 1 ]これにより、凝縮分離は、D完全であるかどうかにかかわらず、モーダス・ポネンスと置換を 持つあらゆる論理システムにとって有用となる。
与えられた大前提と与えられた小前提によって結論が一意に決定されるため（変数名の変更を除いて）、メレディスは、どの 2 つのステートメントが関係しているかをメモするだけでよく、他の表記法を必要とせずに凝縮分離を使用できることに気づきました。これが証明の「D 表記法」につながりました。この表記法では、「D」演算子を使用して凝縮分離を意味し、標準的な接頭辞表記文字列で 2 つの引数を取ります。たとえば、4 つの公理がある場合、D 表記法での典型的な証明は次のようになります。DD12D34 これは、2 つの前の凝縮分離ステップの結果を使用した凝縮分離ステップを示しています。最初のステップでは公理 1 と 2 を使用し、2 番目のステップでは公理 3 と 4 を使用しました。
この表記法は、一部の自動定理証明器で使用されているほか、証明のカタログにも時折登場します。例えば、Metamathの mmsolitaire プロジェクトの「最短の既知の証明」データベースには、このような証明を持つ定理が 196 個掲載されています。[ 3 ]
自動定理証明においては、凝縮分離法は、生のモーダスポネンス法や一様置換法に比べて多くの利点がある。
モーダス・ポネンスと代入法を用いた証明では、変数に代入できる選択肢は無限にあります。つまり、次のステップも無限に考えられます。一方、凝縮分離法では、証明における次のステップは有限個しか考えられません。それは、前のステップや公理を組み合わせた最も一般的なバリエーションに限られます。
完全な簡略化された分離証明のための D 表記法は、カタログ化や検索のために証明を簡単に記述することを可能にします。典型的な完全な 15 ステップの証明は、D 表記法ではわずか 15 文字です (公理の記述を除く)。9 を超える公理または定理を参照することで、少し長くなります。たとえば、複数桁の数字をドットで区切って DD2.10D11DD5.6D9D35.3 と記述できます (ただし、同じ証明で参照番号が最大 35 の場合は DD2aDbDD56D9Dz3 と記述することもできます)。
