Аннотация:
В настоящей работе введено понятие квазитрудноопределяемых формул и исследуются сложности выводов этих формул. Для некоторых классов квазитрудноопределяемых формул получены одинаковые по порядку верхние и нижние оценки шагов выводов в нескольких системах доказательств, основанных на дизъюнктивных нормальных формах (конъюнктивных нормальных формах).
Ключевые слова:proof complexity, Split Tree, resolution system, resolution over linear equations, determinative conjunct, quasi-hard determinative formula.
Поступила в редакцию: 21.03.2011 Принята в печать: 20.04.2011
Полный текст:
PDF файл (480 kB)