On solving the equality problem in theories defined by Horn clauses

DOI10.1016/0304-3975(86)90114-3zbMATH Open0607.03002OpenAlexW1991348109MaRDI QIDQ1085152FDOQ1085152

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

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

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)

Cites Work

• A complete proof of correctness of the Knuth-Bendix completion algorithm
• The Semantics of Predicate Logic as a Programming Language
• A Machine-Oriented Logic Based on the Resolution Principle
• Title not available (Why is that?)
• Complete Sets of Reductions for Some Equational Theories
• Title not available (Why is that?)
• Unit Refutations and Horn Sets
• Proofs by induction in equational theories with constructors
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• Completion of a Set of Rules Modulo a Set of Equations
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Title not available (Why is that?)
• Title not available (Why is that?)
• Proving Theorems with the Modification Method
• The Unit Proof and the Input Proof in Theorem Proving
• Problems and Experiments for and with Automated Theorem-Proving Programs
• Oriented equational clauses as a programming language
• Equational methods in first order predicate calculus

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
• Title not available (Why is that?)
• Title not available (Why is that?)
• Equivalence and difference between institutions: simulating Horn Clause Logic with based algebras
• Title not available (Why is that?)
• The satisfiabilty problem for a class consisting of horn sentences and some non-horn sentences in proportional logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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)