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

Horn clausesequality problemKnuth-Bendix completion procedurenonequational theories

Mathematics Subject Classification ID

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

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

• 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?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• 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
• 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

(12)

• Knuth-bendix completion of horn clause programs for restricted linear resolution and paramodulation
• A maximal-literal unit strategy for horn clauses
• A goal-type driven method of solving Horn logic with equality
• scientific article; zbMATH DE number 3924139 (Why is no real title available?)
• scientific article; zbMATH DE number 4089521 (Why is no real title available?)
• Equivalence and difference between institutions: simulating Horn Clause Logic with based algebras
• 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 1860670 (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?)
• Linear and unit-resulting refutations for 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)