Linearity and regularity with negation normal form

DOI10.1016/J.TCS.2004.09.001zbMATH Open1071.68091OpenAlexW2070794501MaRDI QIDQ703486FDOQ703486

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

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

zbMATH Keywords

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

Mathematics Subject Classification ID

Cites Work

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

Cited In (7)

• The possibilistic Horn non-clausal knowledge bases
• Title not available (Why is that?)
• From Schütte’s Formal Systems to Modern Automated Deduction
• Title not available (Why is that?)
• 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)