ギルモアのアルゴリズム
ここで E ( F ) = { A 1 , A 2 , . . . } {\displaystyle E\left(F\right)=\left\{A_{1},A_{2},...\right\}} はエルブラン領域の要素を述語論理式に代入した基礎例(エルブラン基底)の集合で、アルゴリズムの入力である。 対象となる述語論理式は冠頭標準形にした選言標準形の式で表現される。
実際の手続きは以下のようになる:
k := 1 {\displaystyle k{:=}1} ∧ i = 1 k A i {\displaystyle \wedge _{i=1}^{k}A_{i}} が充足不能(命題論理)でないなら、 k := k + 1 {\displaystyle k{:=}k+1} とし繰り返す 停止する (結果:F は充足不能)
この手続きは半決定可能で、証明したい論理式が充足不能でない場合、手続きは停止しない。一般に、述語論理式が証明可能かどうかは決定可能でないことが知られている。