×

zbMATH — the first resource for mathematics

On the complexity of proof in propositional calculus. (Russian) Zbl 0197.00102
the rule of “expansion”: If \(\alpha\), \(\beta\), \(\gamma\), are variables, neither \(\alpha\) nor \(\overline\alpha\) appearing in \(\Sigma\), \(\alpha\vee\beta\), \(\alpha\vee\gamma\), \(\overline\alpha\vee\overline\beta\vee\overline\gamma\) may be added to \(\Sigma\). The following estimates are proved by a series of graph-theoretical theorems (which might be of independent interest):
\[ (N(\Sigma)+1)/2 \leq L(\Sigma) \leq (3/2)^{N(\Sigma)-1}. \]
2) For every \(c<1/4\) and every \(n\) there is a contradictory system \(\Sigma\), such that
\[ n < c (\log_2\overline N(\Sigma))^2 \leq \log_2L(\Sigma)\quad\text{and}\quad n < (\log_2 L^*(\Sigma))^2 \leq \log_2 L(\Sigma). \]
3) There exists \(c>0\), such that for every \(n\) there is a contradictory system \(\Sigma\), such that
\[ n < c\cdot \root 3\of{N^*(\Sigma)} \leq \log_2 \overline N(\Sigma),\quad n < c\cdot \sqrt{\lambda(\Sigma)} \leq \log_2 \overline N(\Sigma). \]

MSC:
03F20 Complexity of proofs
PDF BibTeX XML Cite
Full Text: EuDML