Article collection "Mathematical Problems of Cybernetics" №14, Moscow, 2005
On the proof complexity in some systems of classical propositional calculi
Proof complexity characteristics in the Frege systems and Frege systems with substitution rule (simple and multiply) are investigated in this paper. For given tautology φ the notion of minimal-determinative disjunctive normal form Ɗmin (φ) is introduced and it is proved that the steps of shortest Frege proof of φ is no more, than c∙s∙Ɩ, where s is some characteristic of Ɗmin (φ), Ɩ is the size of φ and c is some constant, depending of Frege systems choice. It is show also that for given n the sequence of formulas with the size n can be constructed such, that the characteristic s is equal n, n2 , n3 ,…, n[√nlogn 2] . It is proved also, that there exist the sequence of tautologies with the size n, the proof steps and proof sizes of which both in Frege systems and in Frege with substitution are equal by order n and n2 accordingly. Also it is proved that there exist the sequence of tautologies with the size n, the steps of which in the systems with simple substitution are no less than n, while in the systems with multiply substitution are no more than log2 n.
proof complexity characteristics, Frege systems, Frege systems with substitution rule, determinative conjunct, minimal-determinative disjunctive normal form
Publication language:russian, pages:8 (p. 49-56)
Mathematical problems and theory of numerical methods