Completeness for linear regular negation normal form inference systems

\textit{R. Anderson} and \textit{W. W. Bledsoe} [J. Assoc. Comput. Mach. 17, No. 3, 525-534 (1970; Zbl 0199.31502)] introduced a completeness proof of clausal resolution based on an induction on excess literals, i.e., the number of literal occurrences in a clause set \({\mathcal S}\) minus the number of clauses in \({\mathcal S}\). In this paper, the authors use modified forms of the excess literal argument in order to establish completeness proofs for propositional systems based on negation normal form (NNF). First, they recapitulate the completeness proof of (linear) binary resolution with merging for propositional clause sets. Moreover, they show that the tableau method is complete even if the method is restricted to regular connected tableaux and extensions with unit clauses are not allowed. The non-clausal methods for which completeness is stated are the tableau method restricted to regular \(u\)-connected NNF-tableaux without unit extensions and a linear non-clausal (NNF) resolution calculus. Due to space restrictions imposed in conference proceedings, the paper does not contain proofs for the latter completeness results. For the entire collection see [Zbl 0951.00051].

Recommendations

Cited in

(1)

Linearity and regularity with negation normal form

This page was built for publication: Completeness for linear regular negation normal form inference systems

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