Model elimination without contrapositives

DOI10.1007/3-540-58156-1_7zbMath1433.68532OpenAlexW1816816118MaRDI QIDQ5210764

Peter Baumgartner, Ulrich Furbach

Publication date: 21 January 2020

Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-58156-1_7

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (7)

Computing answers with model elimination ⋮ IeanCOP: lean connection-based theorem proving ⋮ Ordered tableaux: Extensions and applications ⋮ Optimizing proof search in model elimination ⋮ Linearity and regularity with negation normal form ⋮ Prolog technology for default reasoning: proof theory and compilation techniques ⋮ An abductive framework for negation in disjunctive logic programming

Uses Software

• SETHEO
• TPTP
• PROTEIN

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Near-Horn prolog and beyond
• Non-Horn clause logic programming without contrapositives
• SETHEO: A high-performance theorem prover
• Consolution as a framework for comparing calculi
• Controlled integration of the cut rule into connection tableau calculi
• A sequent-style model elimination strategy and a positive refinement
• N-Prolog: An extension of prolog with hypothetical implication. II. Logical foundations, and negation as failure
• A comparison of three PROLOG extensions
• The TPTP problem library
• Mechanical Theorem-Proving by Model Elimination
• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness

This page was built for publication: Model elimination without contrapositives