Linearity and regularity with negation normal form

DOI10.1016/j.tcs.2004.09.001zbMath1071.68091OpenAlexW2070794501MaRDI QIDQ703486

Erik Rosenthal, Reiner Hähnle, Neil V. Murray

Publication date: 11 January 2005

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2004.09.001

zbMATH Keywords

Automated theorem provingExcess literal techniqueLinear resolutionNegation normal formNon-clausal resolutionRegular tableauxResolutionTableaux

Mathematics Subject Classification ID

Related Items (5)

ABox abduction in the description logic \(\mathcal{ALC}\) ⋮ A Non-clausal Connection Calculus ⋮ nanoCoP: A Non-clausal Connection Prover ⋮ From Schütte’s Formal Systems to Modern Automated Deduction ⋮ The possibilistic Horn non-clausal knowledge bases

Cites Work

• A theory of diagnosis from first principles
• Completely non-clausal theorem proving
• Linear resolution with selection function
• Dissolution
• Inference with path resolution and semantic graphs
• Special relations in automated deduction
• Theorem Proving via General Matings
• A Deductive Approach to Program Synthesis
• On Matrices with Connections
• Model elimination without contrapositives
• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
• A Computing Procedure for Quantification Theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Linearity and regularity with negation normal form