��������� �. �., ������� �. �.
� �������������� ������������ ���������� ������� � �������� �����

����� ����� �� ������� ���� ������� ������� ������������� ��������� ���������� ����������������� �������, ����������� �������� ��������� ������������������ ����������, ��������� ������� ������� � ���� ������ ������������� ������������� ���������� ������������ (�������������� ������� ��� ������� �������, ������� ���������, �������, ���������� �� ������ �����������, ������� ���������� «Cutting planes», ������������ �������� �����) ����������� ����� ����������� �� ����� ��������� �������. � ��������� ������ ������������, ��� ��� ��������� ������������������� ������ ������ ����� (�����) ������� � �������� ����� ������� �������� �������������������� ������������: ���������� ������ ������������������ ������������������ ������, ������� ������������� ������������ ��������� ������� � ����� ������� �����.

Aleksanyan S. R., Chubaryan A. A.
The polynomial bounds of proof complexity in Frege systems

The concept of a determinative set of variables for a propositional formula was introduced by one of the authors, which made it possible to distinguish the set of hard-determinable formulas. The proof complexity of a formula of this sort has exponential lower bounds in some proof systems of classical propositional calculus (cut-free sequent system, resolution system, analytic tableaux, cutting planes, and bounded Frege systems). In this paper we prove that the property of hard-determinability is insufficient for obtaining a superpolynomial lower bound of proof lines (sizes) in Frege systems: an example of a sequence of hard-determinable formulas is given whose proof complexities are polynomially bounded in every Frege system.

������ ����� ������ / Full texts:

• PDF file (460 KB)
• PostScript file (845 KB)