Horn equational theories and paramodulation
type: Item
instance of: scholarly article
title: Horn equational theories and paramodulation
zbMATH Open document ID: 0682.68091
DOI: 10.1007/BF00248322
author: Ulrich Furbach
author: Steffen Hölldobler
author: Joachim Schreiber
published in: Journal of Automated Reasoning
publication date: 1989-01-01T00:00:00Z
review text: Robinson's pioneering work on mechanizing mathematical logic quite immediately raised the problem ``How can equality axioms be incorporated into resolution machinery ?'' At the same time much effort has been spent on looking for efficient refutationally complete strategies for decidable subclasses of first-order logic. It was then the Prolog language together with Horn clause logic, input and unit resolution were invented giving rise to Logic programming paradigm. A direct proof for the completeness of paramodulation for Horn equality logic (the language of equational logic programs) is presented. The declarative and fixpoint semantics of this language are then investigated, for the operational semantics the inference rules paramodulation and reflection are proven to be sound and complete w.r.t. the fixpoint semantics. It is well-known that automatic theorem provers based on paramodulation are far from being efficient, since they have to explore a search space containing many irrelevant derivations, since paramodulation can be applied both from left to right and from right to left. The commonly used techniques for Logic programming restricting the search space are discussed and demonstrated. Among them are directed paramodulation, conditional term rewriting systems and narrowing. The paper gives a clear and precise vision of the problems, progress and success achieved in the field of equational Logic programming.
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03C52
Mathematics Subject Classification ID: 03C65
zbMATH DE Number: 4117893
zbMATH Keywords: completeness
zbMATH Keywords: paramodulation
zbMATH Keywords: Prolog
zbMATH Keywords: resolution
zbMATH Keywords: Logic programming
zbMATH Keywords: fixpoint semantics
zbMATH Keywords: conditional term rewriting systems
zbMATH Keywords: narrowing
zbMATH Keywords: equational Logic programming
MaRDI profile type: Publication
cites work: Contributions to the Theory of Logic Programming
cites work: Proving Theorems with the Modification Method
cites work: Q5679729
cites work: Incorporating equality into logic programming via surface deduction
cites work: The Semantics of Predicate Logic as a Programming Language
cites work: Oriented equational clauses as a programming language
cites work: Q3765264
cites work: Extending SLD resolution to equational horn clauses using E-unification
cites work: Q3782762
cites work: Q3789061
cites work: Equality, types, modules, and (why not?) generics for logic programming
cites work: Unit Refutations and Horn Sets
cites work: Q3883561
cites work: Q3703312
cites work: A theory of complete logic programs with equality
cites work: An Efficient Unification Algorithm
cites work: Q3339245
cites work: A Technique for Establishing Completeness Results in Theorem Proving with Equality
cites work: Q5678447
cites work: Q5624683
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Q5562604
cites work: Automatic Theorem Proving with Built-in Theories Including Equality, Partial Ordering, and Sets
cites work: Q4770009
cites work: The Concept of Demodulation in Theorem Proving
full work available at URL: https://doi.org/10.1007/bf00248322
OpenAlex ID: W1967047591
description: scientific article; zbMATH DE number 4117893