# 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 { if}} F {\ text {unsatisfiable}} \\ {\ mathrm {\ textit {undef}}}, & {\ text {if}} F {\ text {satisfiable}} \ 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.