重ね合わせの原理

重ね合わせ計算は、等式論理における推論のための計算体系です。1990年代初頭に開発され、一階述語論理の分解の概念と、（不完全な）クヌース・ベンディックス完全性の文脈で開発された順序に基づく等価性処理を組み合わせたものです。これは、分解（等式論理へ）または不完全な完全性（完全な節論理へ）のいずれかの一般化と見なすことができます。ほとんどの一階述語論理と同様に、重ね合わせ計算は、一階述語論理の節の集合の不充足可能性を示そうとします。つまり、反駁によって証明を行います。重ね合わせ計算は反駁完全です。つまり、無制限のリソースと適切な導出戦略があれば、任意の不充足可能な節の集合から、最終的には矛盾が導出されます。

一階述語論理の多くの（最先端の）定理証明器は重ね合わせの原理に基づいている（例えば、E 等式定理証明器など）が、純粋な計算を実装しているものはごくわずかである。

• E
• パス
• 吸血鬼
• ヴァルトマイスター（公式ホームページ）

• 選択と単純化による書き換えベースの等式定理証明、レオ・バッハマイヤーとハラルド・ガンジンガー、論理と計算ジャーナル3(4)、1994年。
• パラモジュレーションに基づく定理証明、ロバート・ニューウェンハイス、アルベルト・ルビオ、自動推論ハンドブックI(7)、エルゼビア・サイエンスおよびMITプレス、2001年。