Equality and abductive residua for Horn clauses
type: Item
instance of: scholarly article
title: Equality and abductive residua for Horn clauses
zbMATH Open document ID: 0788.68133
DOI: 10.1016/0304-3975(93)90243-M
author: P. T. Cox
author: Emanuel Knill
author: Tomasz Pietrzykowski
published in: Theoretical Computer Science
publication date: 1993-12-20T00:00:00Z
review text: This paper presents an approach, called surface deduction, to introduce equality axioms into Horn clause logic in a way to avoid the entailing inefficiency that comes with their unrestricted use. In general, surface deduction refers to a family of transformational methods for reasoning with a theory of equality. A set of input clauses is first transformed to a flat form and symmetrized. The deduction process then proceeds using linear input resolution for Horn clauses, together with a limited use of factoring and a new rule called compression. The flat form of clauses is preserved by the deduction rules. The main effect of flattening is to make the term structure of the clause directly accessible to deduction. Furthermore, surface deduction has proven to be a valuable, analytical tool for understanding the role of equality in abductive reasoning. Additionally, up until now, it is the only nontrivial method for logic programming with equality that can be put to efficient use for this kind of reasoning with little or no loss of explanatory power. However, to use surface deduction in practice on a large scale, it must be enhanced, since the flattening procedure can cause substantial increase in the number of resolution steps, in search complexity and lose most of the advantages of unification. One can retain the advantages of unification and its generalizations by interpreting the set of equalities in the body of a clause as a directed graph or hypergraph. Here, the concise presentation of surface deduction, its characteristics and ramifications provide amble theoretical evidence for the status of this particular deductive inference method. The techniques that have been successful in refutation oriented logic programming should be amenable to be integrated with the ideas proposed to yield an abductively complete and efficient system.
Mathematics Subject Classification ID: 68T27
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 445055
zbMATH Keywords: surface deduction
zbMATH Keywords: Horn clause logic
zbMATH Keywords: abductive reasoning
MaRDI profile type: Publication
cites work: Q3134859
cites work: Proving Theorems with the Modification Method
cites work: Q5688896
cites work: Incorporating equality into logic programming via surface deduction
cites work: Q3782836
cites work: A logical reconstruction of Prolog II
cites work: Foundations of equational logic programming
cites work: Abduction versus closure in causal theories.
cites work: Q3339245
cites work: Linear unification
cites work: A logical framework for default reasoning
cites work: Q5750451
description: scientific article; zbMATH DE number 445055