## 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 edges labeled Ep-unifier equational Horn clauses example ff-derivation 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 substitution instance ground terms Herbrand structure Herbrand universe Herbrand's theorem Horn clause logic Hornlog method interpreted lemma logic program many-sorted first-order language mapping merging model-theoretic Mp,Q n-tuple negation negation normal form negative clause node node chosen node labeled Op,q operational semantics parallel pebbling processor Prolog query Q refutation method rewrite steps sentences sequence set of ground set of Horn set of unifiers set to true sets of variables SLD-resolution sort soundness and completeness subset subterm TERM(P truth field unification Unifsl unsatisfiable iff