ギルモアのアルゴリズム

3行要約

1. 一階述語論理の定理証明において、エルブランの定理に基づく初期の手法。
2. 論理式の充足不能性を判定するために、基底例を順次生成して検証する。
3. 計算効率に課題があったが、後の自動定理証明技術の基礎となった。