The relative complexity of analytic tableaux and SL-resolution (Q687165)

The paper is intended to fill in the gaps in the literature concerning the polynomial simulation relation between proof systems. Roughly, a proof system \(B\) p-simulates a proof system \(A\) if any proof \(\alpha\) of a tautology \(\tau\) in \(A\) can be transformed into a proof \(\beta\) in \(B\) such that the length of \(\beta\) is a polynomial function of the length of \(\alpha\). In the paper, Smullyan's analytic tableau method for propositional calculus is extended and improved to increase its efficiency in proving theorems and analyzing the complexity of proofs. The Improved Parent Clash Restricted (IPCR) method is defined and illustrated by appropriate examples. It is shown that the IPCR method is equivalent to SL-resolution and, hence, both methods p-simulate each other.