バーナイス・シェーンフィンケル級

Concept in first-order logic

ポール・バーネイズ、モーゼス・シェーンフィンケル、フランク・P・ラムゼイにちなんで名付けられた、バーネイズ・シェーンフィンケル類（バーネイズ・シェーンフィンケル・ラムゼイ類とも呼ばれる）の論理式は、充足可能性が決定可能な一階述語論理式の一部である。

これは、冠頭標準形で書かれたときに、量指定子接頭辞を持ち、機能記号を含まない文の集合です。 $\exists ^{*}\forall ^{*}$

ラムゼーは、が1つの自由変数を持つバーネイス-シェーンフィンケル類の式である場合、が有限であるか、またはが有限であることを証明した。^[1] $\phi$ $\{x\in \mathbb {N} :\phi (x)\}$ $\{x\in \mathbb {N} :\neg \phi (x)\}$

このクラスの論理式は、グラウンディングまたはインスタンス化のプロセスによって効果的に命題論理式に変換できるため、効果的に命題的( EPR ) と呼ばれることもあります。

このクラスの充足可能性問題はNEXPTIME完全である。^[2]

アプリケーション

EPRの充足可能性を決定するための効率的なアルゴリズムがSMTソルバーに統合されている。^[3]

^ プラット・ハートマン、イアン（2023年3月30日）『第一階述語論理の断片』オックスフォード大学出版局、186頁。ISBN 978-0-19-196006-2。
^ Lewis, Harry R. (1980)、「量化公式のクラスの計算量結果」、Journal of Computer and System Sciences、21 (3): 317– 353、doi :10.1016/0022-0000(80)90027-6、MR 0603587
^ de Moura, Leonardo; Bjørner, Nikolaj (2008). 「DPLLと置換セットを用いた命題論理の効果的な決定」 . Armando, Alessandro; Baumgartner, Peter; Dowek, Gilles (編).自動推論. コンピュータサイエンス講義ノート. ベルリン, ハイデルベルク: Springer. pp. 410– 425. doi :10.1007/978-3-540-71070-7_35. ISBN 978-3-540-71070-7。

ラムゼー, F. (1930)「形式論理におけるある問題について」, Proc. London Math. Soc. , 30 : 264– 286, doi :10.1112/plms/s2-30.1.264
Piskac, R.; de Moura, L.; Bjorner, N. (2008年12月)、「等価性を考慮した命題論理の効果的な決定」(PDF)、Microsoft Research Technical Report ( 2008– 181)

この数理論理学関連の記事はスタブです。記事を充実させることでWikipediaに貢献できます。