## Graph-based Proof Procedures for Horn Clauses |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

INTRODUCTION | 1 |

PRELIMINARIES | 7 |

A SEMANTICS FOR THE HORNLOG SYSTEM | 21 |

Copyright | |

7 other sections not shown

### Common terms and phrases

algorithm all-solutions protocol answer substitution arity atomic formulae chapter chosen for expansion clause logic clauses with equality computation consisting defined definite clause denotational semantics denoted disjoint equational Horn clauses example ff-graph ff-refutation finite set first-order logic foreach free variables function symbol Gallier goal graph expansion step graph GT(P ground Horn clauses ground terms Herbrand Base Herbrand structure Herbrand universe Herbrand's theorem Horn clause logic Hornlog method Hornlog system interpreted lemma logic program many-sorted first-order language mapping merging model-theoretic n-tuple negation negation normal form negative clause node node chosen node labeled OP,Q operational semantics parallel pebbling processor Prolog query Q rewrite steps sentences sequence set of E-unifiers set of ground set of Horn set to true sets of variables SLD-resolution sort soundness and completeness subset substitution ff subterm TERM(P truth field unification unifier Unifsl unsatisfiable iff