On solving the equality problem in theories defined by Horn clauses
type: Item
instance of: scholarly article
title: On solving the equality problem in theories defined by Horn clauses
zbMATH Open document ID: 0607.03002
DOI: 10.1016/0304-3975(86)90114-3
author: B. George
published in: Theoretical Computer Science
publication date: 1986-01-01T00:00:00Z
review text: The Knuth-Bendix completion procedure for solving the equality problem in equational theories is adapted to nonequational theories defined by sets of Horn clauses. Completeness can be achieved by endowing the procedure with a weak axiomatization of Boolean calculus and the reflexivity axiom for equality. It is shown that the procedure can also be used for inductive proofs, i.e., for proving universally quantified formulas in the initial model defined by a set of Horn clauses. The relationships to some resolution and paramodulation methods are discussed, and experimental results are appended.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B25
zbMATH DE Number: 3981149
zbMATH Keywords: Knuth-Bendix completion procedure
zbMATH Keywords: equality problem
zbMATH Keywords: nonequational theories
zbMATH Keywords: Horn clauses
reviewed by: Manfred Armbrust
MaRDI profile type: Publication
full work available at URL: 0304-3975(86)90114-3
OpenAlex ID: W1991348109
cites work: Proving Theorems with the Modification Method
cites work: The Unit Proof and the Input Proof in Theorem Proving
cites work: Q5679729
cites work: The Semantics of Predicate Logic as a Programming Language
cites work: Oriented equational clauses as a programming language
cites work: Q3336735
cites work: Q3962973
cites work: Q3674088
cites work: Proofs by induction in equational theories with constructors
cites work: Unit Refutations and Horn Sets
cites work: A complete proof of correctness of the Knuth-Bendix completion algorithm
cites work: Q3786024
cites work: Completion of a Set of Rules Modulo a Set of Equations
cites work: Q3709891
cites work: Q3338226
cites work: Q5581665
cites work: Problems and Experiments for and with Automated Theorem-Proving Programs
cites work: Equational methods in first order predicate calculus
cites work: Q3347863
cites work: A Technique for Establishing Completeness Results in Theorem Proving with Equality
cites work: Q5678447
cites work: Complete Sets of Reductions for Some Equational Theories
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
Recommended article: Q3698310
Recommended article: Automated Deduction – CADE-20
Recommended article: Complexity of the problem of being equivalent to Horn formulas
Recommended article: The Essentially Equational Theory of Horn Classes
Recommended article: Complexity of the problem of being equivalent to Horn formulas. II
Recommended article: Efficient deduction in equality Horn logic by Horn-completion
Recommended article: Equality and abductive residua for Horn clauses
Recommended article: A goal-type driven method of solving Horn logic with equality
Recommended article: Q3212269
description: scientific article; zbMATH DE number 3981149