Graph-based proof procedures for horn clauses (Q1188938): Difference between revisions

The monograph presents ``Hornlog'', a proof procedure for Horn clauses with negation in its logical semantics, rather than negation by failure. The nodes of the graph are the intermediate goals and the edges are labelled with control information. Compared to SLD resolution, where the corresponding structure is a tree, Hornlog needs a graph because common subgoals are identified and cycles are recognized. The procedure comes in two versions, one for Horn clauses without equality and the other one with equality. Equality is handled in an E-resolution style. Therefore it is implementable only for the restricted case where for the equations there is an equivalent E-unification algorithm. The method is described in a detailed mathematical formalism. Proofs for the soundness and completeness of the method with respect to a model theoretic semantics are provided. Its application to logic programming is discussed and an implementation on a MIMD parallel computer is described. The monograph, which actually is the author's PhD thesis, is not a general introduction into theorem proving and logic programming, but it is self-contained with respect to the mathematics used.