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.