Gilmore's algorithm

from Wikipedia, the free encyclopedia

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:

Let the countable set be the Herbrand expansion to F and serve as the input of the algorithm.


  • As long as it can be fulfilled (propositionally), set
  • 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.