"Записки научных семинаров ПОМИ"

Том 407, стр. 111-128

СС.-Петербургское отделение Математического института им. В. А. Стеклова РАН, Фонтанка 27, 191023 Санкт-Петербург, Россия

orevkov@pdmi.ras.ru

Аннотация: В работе метод резолюций расширяется новым правилом, которое аналогично правилу сечения генценовских секвенциальных исчислений. Получены верхние и нижние оценки сложности опровержений с аналогом правила сечения и без этого правила. Сложность опровержений сравнивается также со сложностью секвенциальных доказательств с сечениями по формулам, которые не содержат импликаций, конъюнкций и квантора $\exists$ и в которые отрицание может входить только непосредственно перед элементарными формулами. Библ. -- 3 назв.
Ключевые слова:метод резолюций, опровержение, сечение, секвенция, верхняя оценка, нижняя оценка [Resolution Method, refutation, cut, sequent, upper bound, lower bound]