Linear and unit-resulting refutations for Horn theories

DOI10.1007/BF00252179zbMath0860.03013OpenAlexW2136382758MaRDI QIDQ1923821

Peter Baumgartner

Publication date: 21 April 1997

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

Full work available at URL: https://doi.org/10.1007/bf00252179

zbMATH Keywords

Horn clauseHorn theoryunit resolutionfirst-order clause logiclinear strategymodel-eliminationredundancy criterion

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Tree-like unit refutations in Horn constraint systems, Incremental theory reasoning methods for semantic tableaux

Uses Software

• SETHEO
• TPTP
• PROTEIN

Cites Work

• 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
• 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