Пятница, 5 апреля, ауд. 106. Начало в 17:00.
Докладчик: С.И. Грязнов.
Тема: Нижние оценки в древовидной системе доказательств Res(+) на ordering principles.
Abstract
Система доказательств Res(+), предложенная Ицыксоном и Соколовым, -- расширение резолюционной системы доказательств. Она оперирует с дизъюнкциями линейных равенств над
![$ F_2 $](../../../sites/default/files/tex/4d7738c408e9a1d6d505477f44643a5544a0b9cf/index.png)
. В докладе мы рассмотрим технику доказательства нижних оценок на размер доказательств некоторых противоречивых семейств формул для древовидной Res(+), основанную на играх Прувера и Дилеера. Данная техника является обобщением доказательства нижней оценки для принципа Дирихле. Затем мы применим данную технику для доказательства нижних оценок на Ordering principle и Dense Linear Ordering principle.
Ordering principle утверждает, что не существует конечного линейного порядка без минимума. Мы дадим нижнюю оценку
![$ 2^{n−O(1)} $](../../../sites/default/files/tex/9e869934ee945bf077fa7aa9dfe260f4f4a1dc5d/index.png)
на размер любого древовидного Res(+) доказательства этого утверждения, записанного в КНФ. Dense Linear Ordering principle утверждает, что не существует конечных плотных линейных порядков. Мы дадим
![$ 2^{n/3−O(1)} $](../../../sites/default/files/tex/53ce1cfe25b89862de890aa4008f54d2e8247bce/index.png)
нижнюю оценку на размер любого древовидного Res(+) доказательства этого утверждения, записанного в КНФ.
Ordering principle и Dense Linear Ordering principle имеют доказательство полиномиального размера в резолюциях. Таким образом, мы приведем естественные примеры, разделяющие древовидную версию системы Res(+) и резолюцию.