The Hornlog Proof Procedure

  • Stan Raatz
Part of the Progress in Computer Science and Applied Logic book series (PCS, volume 10)


In this chapter we develop the Hornlog proof procedure. The method, which is inspired by Herbrand’s theorem, incrementally builds a graph in a way that encodes a first-order quantifier-free formula, and then checks for unsatisfiability of this formula using a linear-time algorithm [14]. The low polynomial complexity is important, since all computational logic methods can be understood as instances of Herbrand’s reduction of the provability (and therefore unsatisfiability) of first-order formula A to the provability of a set of ground instances of A. If the test for provability in the ground case is expensive, there is little likelihood that an efficient implementation of the method exists. If the check for unsatisfiability fails, the graph is rewritten by choosing a node and expanding it, and the expanded graph is again checked for unsatisfiability. The process terminates if the graph is shown to be unsatisfiable, or if it can no longer be expanded, in which case the query formula is shown to be refutable. The process may also enter into a non-terminating sequence of expansion steps. The algorithm that checks for unsatisfiability is not a resolution method, and has the property that the truth of each node is checked at most once.


Logic Program Atomic Formula Horn Clause Attribute Grammar Mature Node 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media New York 1990

Authors and Affiliations

  • Stan Raatz
    • 1
  1. 1.Department of Computer ScienceRutgers UniversityNew BrunswickUSA

Personalised recommendations