## 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 | 6 |

PRELIMINARIES | 7 |

A SEMANTICS FOR THE HORNLOG SYSTEM | 21 |

Copyright | |

7 other sections not shown

### Other editions - View all

### Common terms and phrases

3xnQ algorithm all-solutions protocol answer substitution arity atomic formulae chapter chosen for expansion clause logic clauses with equality computation consisting defined definite clause denoted disjoint E-unifiers 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 substitution instance ground terms H-derivation 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 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 rewrite steps sentences sequence set of ground set of Horn set of unifiers set to true sets of variables sort soundness and completeness subset subterm TERM(P tn/xn truth field unification Unifsl unsatisfiable iff