Incorporating equality into logic programming via surface deduction
type: Item
instance of: scholarly article
title: Incorporating equality into logic programming via surface deduction
zbMATH Open document ID: 0609.68067
DOI: 10.1016/0168-0072(86)90069-2
author: P. T. Cox
author: Tomasz Pietrzykowski
published in: Annals of Pure and Applied Logic
publication date: 1986-01-01T00:00:00Z
review text: In this account the authors exploit the idea of a special deduction mechanism for logic programming called surface-deduction, henceforth s- deduction for short. They claim that this kind of deduction mechanism copes successfully with the problem of finding a refutation for any set of Horn clauses which is unsatisfiable in standard equational theory. To apply s-deduction correctly, arbitrary Horn clauses to be resolved upon are subjected to transformation into special Horn clauses labelled ''flat clauses''. This flattening also takes appropriate care of the prevailing symmetric property of equality in decomposing input clauses into flat ones. A flat clause satisfies the following structure constraints: Only variables are allowed as arguments for non-equality predicates and at most one non-variable subterm, constructed merely upon variable subterms, occurring always on the right hand side of equality predicates. Flattening is proved to be a sound, complete and terminating closure-operation on arbitrary Horn clauses. S-deduction operates on these flat clauses according to three resolution rules, coined surface resolution, surface factoring and compression, all of them preserving the flatness property of the clauses they are applied to. S-deduction's soundness and completeness in the presence of standard equality is formally shown. Both of them remain valid even for sets of Horn clauses non-incorporating equality at all. Again special lemma-based credit is given to the important and computationally troublesome symmetric property of equality. Further on s-deduction evolves as an extension of Colmerauer's approach in PROLOG II to tune efficiency tackling the problem of unification of certain nonunifiable terms by introducing the standard equality axioms. Thus the detection of non-unifiability caused by conflicts of constants or deduction cycles is rendered more feasible and even provides valuable and applicable means for control whereever and whenever appropriate. Run- ti…
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68N01
zbMATH DE Number: 3986673
zbMATH Keywords: logic programming
zbMATH Keywords: refutation
zbMATH Keywords: Horn clauses
zbMATH Keywords: flat clauses
zbMATH Keywords: surface resolution
zbMATH Keywords: standard equality
zbMATH Keywords: unification
zbMATH Keywords: non-unifiability
MaRDI profile type: Publication
full work available at URL: 0168-0072(86)90069-2
OpenAlex ID: W2043837816
cites work: A logical reconstruction of Prolog II
cites work: Linear unification
cites work: Q5624683
cites work: Q5537599
description: scientific article; zbMATH DE number 3986673