Gilmore's algorithm

The Gilmore algorithm (also Gilmore algorithm ) is based on Herbrand's theorem and provides a semi-decision procedure to test predicate logic formulas for unsatisfiability. The following applies:

${\displaystyle \operatorname {\textit {Gilmore}} \left(E\left(F\right)\right)={\begin{cases}{\mathrm {\textit {halt}} },&{\text{wenn }}F{\text{ unerfüllbar}}\\{\mathrm {\textit {undef}} },&{\text{wenn }}F{\text{ erfüllbar}}\end{cases}}}$

Let the countable set be the Herbrand expansion to F and serve as the input of the algorithm. ${\displaystyle E\left(F\right)=\left\{A_{1},A_{2},...\right\}}$

Pseudocode:

• ${\displaystyle k{:=}1}$
• As long as it can be fulfilled (propositionally), set ${\displaystyle \bigwedge _{i=1}^{k}A_{i}}$ ${\displaystyle k{:=}k+1}$
• Stop. (Output: unsatisfiable )

One can see that the algorithm is semi-decidable , since it only lasts in a finite time if it determines that it cannot be fulfilled.