Пятница 05.04. С.И. Грязнов: "Нижние оценки в древовидной системе доказательств Res(+) на ordering principles"

Докладчик: 
С.И. Грязнов
Дата: 
Friday, April 5, 2019 - 17:00
Место: 
ауд. 106
Аннотация: 

Система доказательств Res(+), предложенная Ицыксоном и Соколовым, -- расширение резолюционной системы доказательств. Она оперирует с дизъюнкциями линейных равенств над $F_2$. В докладе мы рассмотрим технику доказательства нижних оценок на размер доказательств некоторых противоречивых семейств формул для древовидной Res(+), основанную на играх Прувера и Дилеера. Данная техника является обобщением доказательства нижней оценки для принципа Дирихле. Затем мы применим данную технику для доказательства нижних оценок на Ordering principle и Dense Linear Ordering principle.

Ordering principle утверждает, что не существует конечного линейного порядка без минимума. Мы дадим нижнюю оценку $2^{n−O(1)}$ на размер любого древовидного Res(+) доказательства этого утверждения, записанного в КНФ. Dense Linear Ordering principle утверждает, что не существует конечных плотных линейных порядков. Мы дадим $2^{n/3−O(1)}$ нижнюю оценку на размер любого древовидного Res(+) доказательства этого утверждения, записанного в КНФ.

Ordering principle и Dense Linear Ordering principle имеют доказательство полиномиального размера в резолюциях. Таким образом, мы приведем естественные примеры, разделяющие древовидную версию системы Res(+) и резолюцию.