Article collection "Mathematical Problems of Cybernetics" №14, Moscow, 2005

Authors:Chubaryan A.A.

On the proof complexity in some systems of classical propositional calculi

Abstract:

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, n^{2} , n^{3} ,…, 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 n^{2} 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 log_{2} n.

Keywords:

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)

Research direction:

Mathematical problems and theory of numerical methods