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 . 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.