Linear and unit-resulting refutations for Horn theories
type: Item
instance of: scholarly article
title: Linear and unit-resulting refutations for Horn theories
zbMATH Open document ID: 0860.03013
DOI: 10.1007/BF00252179
author: Peter Baumgartner
published in: Journal of Automated Reasoning
publication date: 1997-04-21T00:00:00Z
review text: The paper presents an approach to combine two effective resolution strategies for a Horn clause set. The proposed method consists of saturating a Horn clause set under several deduction operations by adding new inference rules until only redundant consequences can be added. This technique -- called linearizing completion -- allows to combine the unit-resulting resolution strategy with a linear strategy à la Prolog in a refutationally complete way. This is not trivial, since although each strategy alone is complete for Horn theories, their naive combination is not. A redundancy criterion allows deletion of many of added inference rules, which makes the resulting inference systems quite compact. The transformed theory can be used in combination with linear calculi, such as, e.g., model elimination, to yield sound, complete and efficient calculi for full first-order clause logic over the given Horn theory. The method has been implemented and has been tested in conjunction with a model-elimination theorem prover.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 934090
zbMATH Keywords: unit resolution
zbMATH Keywords: Horn clause
zbMATH Keywords: linear strategy
zbMATH Keywords: redundancy criterion
zbMATH Keywords: first-order clause logic
zbMATH Keywords: Horn theory
zbMATH Keywords: model-elimination
reviewed by: Nail Zamov
describes a project that uses: SETHEO
describes a project that uses: TPTP
describes a project that uses: PROTEIN
MaRDI profile type: Publication
cites work: Equational inference, canonical proofs, and proof orderings
cites work: Q4264723
cites work: Q3809306
cites work: Consolution as a framework for comparing calculi
cites work: Q4261066
cites work: Q4255506
cites work: Challenge problems in elementary calculus
cites work: Q4012176
cites work: A resolution principle for a logic with restricted quantifiers
cites work: Q5679729
cites work: Proving termination with multiset orderings
cites work: Orderings for term-rewriting systems
cites work: Computing with rewrite systems
cites work: Termination of rewriting
cites work: Q4012174
cites work: Q4036569
cites work: Z-Resolution: Theorem-Proving with Compiled Axioms
cites work: Horn equational theories and paramodulation
cites work: Rigid E-unification: NP-completeness and applications to equational matings
cites work: A completion procedure for conditional equations
cites work: Q3490996
cites work: Foundations of equational logic programming
cites work: Q3674088
cites work: Q3028369
cites work: Q3883561
cites work: Simplifying conditional term rewriting systems: Unification, termination and confluence
cites work: Q5581665
cites work: SETHEO: A high-performance theorem prover
cites work: Controlled integration of the cut rule into connection tableau calculi
cites work: Q3339245
cites work: Mechanical Theorem-Proving by Model Elimination
cites work: Q5600875
cites work: Q4139711
cites work: Special relations in automated deduction
cites work: Q4016555
cites work: Complexity and related enhancements for automated theorem-proving programs
cites work: Q4264721
cites work: Equational methods in first order predicate calculus
cites work: On solving the equality problem in theories defined by Horn clauses
cites work: Q4013363
cites work: A sequent-style model elimination strategy and a positive refinement
cites work: Q5624683
cites work: Unification theory
cites work: Automated deduction by theory resolution
cites work: A Prolog technology theorem prover: A new exposition and implementation in Prolog
cites work: Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
cites work: The TPTP problem library. CNF release v1. 2. 1
cites work: The linked inference principle. I: The formal treatment
cites work: Q3789100
full work available at URL: https://doi.org/10.1007/bf00252179
OpenAlex ID: W2136382758
description: scientific article; zbMATH DE number 934090