Linearity and regularity with negation normal form

DOI10.1016/J.TCS.2004.09.001MaRDI QIDQ703486zbMATH OpenOpenAlexFDO

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

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

Recommendations

• scientific article; zbMATH DE number 1090101
• The Completeness of Propositional Resolution: A Simple and Constructive Proof
• Generalized resolution and NC-resolution
• On linear resolution
• scientific article; zbMATH DE number 4210103

Cites work

• scientific article; zbMATH DE number 3568056 (Why is no real title available?)
• scientific article; zbMATH DE number 1090101 (Why is no real title available?)
• scientific article; zbMATH DE number 834572 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• scientific article; zbMATH DE number 1395652 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• scientific article; zbMATH DE number 3310921 (Why is no real title available?)
• scientific article; zbMATH DE number 3349332 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A Deductive Approach to Program Synthesis
• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
• A theory of diagnosis from first principles
• Completely non-clausal theorem proving
• Dissolution
• Inference with path resolution and semantic graphs
• Linear resolution with selection function
• Model elimination without contrapositives
• On Matrices with Connections
• Resolution theorem proving
• Special relations in automated deduction
• Tableaux and related methods
• Theorem Proving via General Matings

Cited in

(7)

• The possibilistic Horn non-clausal knowledge bases
• scientific article; zbMATH DE number 1090101 (Why is no real title available?)
• From Schütte’s Formal Systems to Modern Automated Deduction
• scientific article; zbMATH DE number 847079 (Why is no real title available?)
• ABox abduction in the description logic \(\mathcal{ALC}\)
• A Non-clausal Connection Calculus
• nanoCoP: a non-clausal connection prover

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

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