On solving the equality problem in theories defined by Horn clauses

DOI10.1016/0304-3975(86)90114-3MaRDI QIDQ1085152zbMATH OpenOpenAlexFDO

Authors B. George

Publication date 1986

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(86)90114-3

zbMATH Keywords

equality problemHorn clausesKnuth-Bendix completion procedurenonequational theories

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

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.

Recommendations

• scientific article; zbMATH DE number 3924139
• Automated Deduction – CADE-20
• Complexity of the problem of being equivalent to Horn formulas
• The Essentially Equational Theory of Horn Classes
• Complexity of the problem of being equivalent to Horn formulas. II
• Efficient deduction in equality Horn logic by Horn-completion
• Equality and abductive residua for Horn clauses
• A goal-type driven method of solving Horn logic with equality
• scientific article; zbMATH DE number 4195157

Cites work

• A complete proof of correctness of the Knuth-Bendix completion algorithm
• A Machine-Oriented Logic Based on the Resolution Principle
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• Complete Sets of Reductions for Some Equational Theories
• Completion of a Set of Rules Modulo a Set of Equations
• Equational methods in first order predicate calculus
• scientific article; zbMATH DE number 3870639 (Why is no real title available?)
• scientific article; zbMATH DE number 3871335 (Why is no real title available?)
• scientific article; zbMATH DE number 3891336 (Why is no real title available?)
• scientific article; zbMATH DE number 3829296 (Why is no real title available?)
• scientific article; zbMATH DE number 3938563 (Why is no real title available?)
• scientific article; zbMATH DE number 4049135 (Why is no real title available?)
• scientific article; zbMATH DE number 3784848 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• Oriented equational clauses as a programming language
• Problems and Experiments for and with Automated Theorem-Proving Programs
• Proofs by induction in equational theories with constructors
• Proving Theorems with the Modification Method
• The Semantics of Predicate Logic as a Programming Language
• The Unit Proof and the Input Proof in Theorem Proving
• Unit Refutations and Horn Sets

Cited in

(14)

• Efficient deduction in equality Horn logic by Horn-completion
• Linear and unit-resulting refutations for Horn theories
• A goal-type driven method of solving Horn logic with equality
• scientific article; zbMATH DE number 1004365 (Why is no real title available?)
• The satisfiabilty problem for a class consisting of horn sentences and some non-horn sentences in proportional logic
• scientific article; zbMATH DE number 3924139 (Why is no real title available?)
• scientific article; zbMATH DE number 4089521 (Why is no real title available?)
• scientific article; zbMATH DE number 176740 (Why is no real title available?)
• scientific article; zbMATH DE number 4118335 (Why is no real title available?)
• scientific article; zbMATH DE number 1860670 (Why is no real title available?)
• Equivalence and difference between institutions: simulating Horn Clause Logic with based algebras
• A maximal-literal unit strategy for horn clauses
• Knuth-bendix completion of horn clause programs for restricted linear resolution and paramodulation
• On word problems in Horn theories

This page was built for publication: On solving the equality problem in theories defined by Horn clauses

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1085152)