Aspects of a graph-based proof procedure for horn clauses
Stan Raatz, Jean H. Gallier · 1987
This dissertation explores several topics concerning HORNLOG, a graph-based proof procedure for Horn clauses which has application to logic programming. After an introductory chapter, in chapter 2, we present the method, which admits one-sorted Horn clause programs consisting of any arbitrary Horn clause, including clauses of the form $\gets B\sb1,\dots,B\sb{n}$, and queries of the form $Q$ = $\exists x\sb1\dots$ $\exists x\sb{n}( eg H\sb1\vee\cdots\vee eg H\sb{m})$ where $\{ eg H\sb1,\dots,H\sb{m}\}$ are one-sorted Horn clauses whose sets of variables are disjoint, and where $\{x\sb1,\dots,x\sb{n}\}$ is the union of all these variables. This class of formulae can result in answers which are indefinite, in the sense that an answer can consist of a disjunction of substitutions. The method is based on a form of graph-rewriting and a linear-time algorithm for testing the unsatisfiability of propositional Horn formulae. We give constructive proofs of the soundness and completeness of the answer substitution, and show the relationship between the operational semantics of the method and the model-theoretic semantics of the underlying language. In chapter 3, we define an equational extension HORNLOG, the $HE\sp\dagger$-refutation method, which applies to many-sorted first-order equational Horn clause programs consisting of clauses of the form $s\doteq$ t, A $\gets B\sb1,\dots,B\sb{n},$ or $\gets B\sb1,\dots,B\sb{n}$ where s and t are first-order terms, A is a non-equational atomic formula, and $B\sb1,\dots,B\sb{n}$ are either equational or non-equational atomic formulae. This class of programs subsumes the paradigms of functional, logic, and equational programming. The method is shown to be complete for E-unification procedures which enumerate a complete set of E-unifiers. In chapter 4 we describe in detail serial implementations of the methods, and consider the design of implementations on a abstract parallel machine.