Linear and unit-resulting refutations for Horn theories

DOI10.1007/BF00252179zbMath0860.03013MaRDI QIDQ1923821

Peter Baumgartner

Publication date: 21 April 1997

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

Horn clause; Horn theory; unit resolution; first-order clause logic; linear strategy; model-elimination; redundancy criterion

Mathematics Subject Classification ID

DB lookup for MSC labels failed

Uses Software

• SETHEO
• TPTP
• PROTEIN

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Orderings for term-rewriting systems
• A completion procedure for conditional equations
• Challenge problems in elementary calculus
• Rigid E-unification: NP-completeness and applications to equational matings
• Equational methods in first order predicate calculus
• On solving the equality problem in theories defined by Horn clauses
• Termination of rewriting
• Simplifying conditional term rewriting systems: Unification, termination and confluence
• Unification theory
• SETHEO: A high-performance theorem prover
• The linked inference principle. I: The formal treatment
• A Prolog technology theorem prover: A new exposition and implementation in Prolog
• Complexity and related enhancements for automated theorem-proving programs
• The TPTP problem library. CNF release v1. 2. 1
• Consolution as a framework for comparing calculi
• Controlled integration of the cut rule into connection tableau calculi
• Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
• A resolution principle for a logic with restricted quantifiers
• Foundations of equational logic programming
• Automated deduction by theory resolution
• Horn equational theories and paramodulation
• A sequent-style model elimination strategy and a positive refinement
• Z-Resolution: Theorem-Proving with Compiled Axioms
• Computing with rewrite systems
• Special relations in automated deduction
• Proving termination with multiset orderings
• Equational inference, canonical proofs, and proof orderings
• Mechanical Theorem-Proving by Model Elimination