Алексанян С. Р., Чубарян А. А.
О полиномиальных ограничениях сложностей выводов в системах Фреге

Ранее одним из авторов было введено понятие определяющего множества переменных пропозициональной формулы, позволившее выделить множество трудноопределяемых тавтологий, сложности выводов которых в ряде систем доказательств классического исчисления высказываний (секвенциальной системе без правила сечения, системе резолюций, системе, основанной на методе расщепления, системе неравенств «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)