エルブランの定理

3行要約

1. 一階述語論理の妥当性を、命題論理の有限集合の充足不能性に帰着させる論理学の定理。
2. コンピュータによる自動定理証明の理論的基盤となり、解像原理などの手法を生み出した。
3. 数学的証明の構造をアルゴリズム的に解析することを可能にした、重要な成果である。