Linear and unit-resulting refutations for Horn theories

DOI10.1007/BF00252179zbMATH Open0860.03013OpenAlexW2136382758MaRDI QIDQ1923821FDOQ1923821

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)

Cites Work

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

Cited In (3)

• A new combination of input and unit deductions for Horn sentences
• Incremental theory reasoning methods for semantic tableaux
• Tree-like unit refutations in Horn constraint systems

Uses Software

• SETHEO
• TPTP
• PROTEIN

This page was built for publication: Linear and unit-resulting refutations for Horn theories

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