7 - Метод резолюций. Скулемовские функции. Метод резолюций для исчисления высказываний. Метод резолюций для исчисления предикатов (Конспект лекций)

ÔÍ-12ÔÍ-12ÌÃÒÓМосковский государственный технический университетимени Н.Э. БауманаÌÃÒÓФакультет «Фундаментальные науки»Кафедра «Математическое моделирование»ÌÃÒÓÀ.Í. ÊàíàòíèêîâÈ ÒÅÎÐÈß ÀËÃÎÐÈÒÌÎÂÊîíñïåêò ëåêöèéÔÍ-12Москва2009ÌÃÒÓÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12Äëÿ ñòóäåíòîâ êàôåäðû ÈÓ9ÌÃÒÓÌÃÒÓÌÀÒÅÌÀÒÈ×ÅÑÊÀß ËÎÃÈÊÀÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓ7.1. Скулемовские функции∃x1 . . .

∃xr−1 ∃xr ∇xr+1 . . . ∇xk X ⇒ ∃x1 . . . ∃xr−1 ∇xr+1 . . . ∇xk Xcxrr .∃x∀y∀z∃u∀v∃wP (x, y, z, u, v, w).В префиксе формулы три квантора существования. Левее ∃x нет кванторов всеобщности.Поэтому первый шаг — замена переменной x константой. Получим:∀y∀z∃u∀v∃wP (c1 , y, z, u, v, w).70ÔÍ-12Пример 7.1. Построим скулемовскую стандартную форму для формулыÌÃÒÓПусть i1 , i2 , . . . , is — список номеров всех кванторов всеобщности, предшествующих кванторнойприставке ∃xr . Вводим новый функциональный символ f , тип которого определяется последовательностью сортов переменных xr , xi1 , xi2 , . .

. , xis , затем в формуле X каждое вхождениепеременной xr заменяем термом f (xi1 , xi2 , . . . , xis ), а кванторную приставку ∃xr из префиксаудаляем.Добавляемые в описанной процедуре константы и функциональные символы называют скулемовскими функциями, а полученную формулу в предваренной форме без кванторов существования с матрицей в конъюнктивной нормальной форме — скулемовской стандартнойформой.ÔÍ-12Напомним, что любая формула алгебры предикатов может быть приведена к предвареннойформе, т.е.

форме вида ∇x1 ∇x2 . . . ∇xk X[x1 , x2 , . . . , xk ], где формула X (матрица предвареннойформы) не имеет кванторов, а символ ∇ обозначает один из кванторов.Формула X, как бескванторная, может быть преобразована в экививалентную конъюнктивную нормальную форму. В исчислении высказываний это можно сделать через таблицыистинности, но более эффективно (а в исчислении предикатов и неизбежно) использовать методэквивалентных преобразований. Достаточно выразить все импликации и эквиваленции черезотрицание, дизъюнкцию и конъюнкцию, а затем преобразовать формулу по законом булевойалгебры, рассматривая конъюнкцию как сложение, а дизъюнкцию как умножение.Следующий шаг — такое преобразование предваренной формы, при котором в ее префиксенет кванторов существования.

Делается это путем расширения языка с добавлением константи функциональных символов следующим образом. Пусть кванторная приставка ∇xr содержитквантор существования, т.е. имеет вид ∃xr . Если левее ее в префиксе нет кванторов всеобщности, выбираем константу as , не содержащуюся в формуле X, в этой формуле заменяем всевхождения переменной xr на константу cr и кванторную приставку удаляем:ÌÃÒÓÔÍ-12ÌÃÒÓОдно из прикладных направлений развитие логики — автоматический поиск доказательств.Основу для соответствующих алгоритмов составляют формальные системы генценовского типа, в которых вывод секвенций обладает высокой алгоритмичностью. И хотя, как было доказано, не существует универсальной разрешающей процедуры для построения вывода любойформулы или ее опровержения, генценовский вывод показывает, что для многих формул конечная разрешающая процедура существует.Мы рассмотрим один из подходов к решению поставленной проблемы — так называемыйметод резолюций.

Он приспособлен для формул исчисления предикатов (или высказываний)определенного вида. Оказывается, что любая формула может быть преобразована в эквивалентную форму, пригодную для применения метода резолюций.ÔÍ-12ÔÍ-127. МЕТОД РЕЗОЛЮЦИЙÃÒÓÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓ71Перед приставкой ∃u два квантора существования. Поэтому переменную u меняем на двуместный функциональный символ:∀y∀z∀v∃wP (c1 , y, z, f1 (y, z), v, w).перед приставкой ∃w три квантора всеобщности. Значит, используем трехместный функциональный символ:∀y∀z∀vp(c1 , y, z, f1 (y, z), v, f2 (y, z, v)).ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓ7. Метод резолюцийÔÍ-12Последняя формула и есть скулемовская стандартная форма.Пример 7.2. Построим скулемовскую стандартную форму для формулы∀x∃y∃z((¬p(x, y) ∧ q(y, z)) ∨ r(x, y, z)).∀x [¬p(x, f1 (x)) ∨ r(x, f1 (x), f2 (x))] ∧ [q(f1 (x), f2 (x)) ∨ r(x, f1 (x), f2 (x))] .Теорема 7.1.

Пусть S — множество дизъюнктов из стандартной формы для формулы F .Тогда формула F противоречива в том и только в том случае, когда множество дизъюнктов Sпротиворечиво.ÔÍ-12J Мы сразу можем считать, что формула F дана в предваренной форме. В принципе убиратькванторы существования можно в любом порядке (эти операции независимы и отличаются лишьвыбором свободных констант и функциональных символов). Но удобнее это делать в порядкеслева направо. Более того, достаточно доказать, что условие противоречивости сохраняетсяпри убирании одного квантора.Пусть формула F имеет вид F = ∃x1 X. В соответствии с описанной процедурой преобразованная форула будет иметь вид Fe = Xcx11 .

Ложность F равносильна истинности ¬F ≡ ∀x1 ¬Xили, что то же самое, истинности ¬X при любой интерпретации и любой оценке. Замена x1 наконстанту лишь переносит конкретизацию значения x1 из сферы оценки в сферу интерпретации.ÌÃÒÓЧтобы объяснить смысл описанного преобразования формул, введем несколько понятий.литера — это элементарная формула алгебры предикатов или ее отрицание. Дизъюнкциянескольких литер называют дизъюнктом. Иногда дизъюнкт удобно интерпретировать какмножество литер, а не их дизъюнкцию. При этом пустое множество литер представляет собойпустой дизъюнкт, который обозначают символом “. Считают, что пустой дизъюнкт —”всегда ложная формула. Далее будем рассматривать конечные множества дизъюнктов.

Такоемножество является формой представления конъюнкции всех дизъюнктов этого множества. Отсюда вытекает понятие противоречивого множества дизъюнктов как множества дизъюнктов,конъюнкция которых, замкнутая кванторами всеобщности, дает противоречие (т.е. формула,ложная в любой интерпретации).В скулемовской стандартной форме матрицу как КНФ можно интерпретировать как множество нескольких дизъюнктов. Мы также считаем, что каждая свободная переменная связанаквантором всеобщности.

Суть преобразования к стандартной форме — в сохранении условияпротиворечивости.ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓНаконец, убираем и второй квантор существования:ÌÃÒÓÔÍ-12∀x∃z [¬p(x, f1 (x)) ∨ r(x, f1 (x), z)] ∧ [q(f1 (x), z) ∨ r(x, f1 (x), z)] .ÔÍ-12ÌÃÒÓДалее элиминируем (т.е. убираем) первый слева квантор существования:ÌÃÒÓÔÍ-12∀x∃y∃z [¬p(x, y) ∨ r(x, y, z)] ∧ [q(y, z) ∨ r(x, y, z)] .ÔÍ-12ÔÍ-12Первый шаг — приведение матрицы приведенной формы к КНФ:ÌÃÒÓÌÃÒÓПредположим, что формула F имеет вид F = ∀x1 ∀x2 .

. . ∀xr−1 ∃xr X. В соответствии справилом удаления квантора существования преобразованная формула будет иметь вид Fe =r. Ложность формулы F в данной интерпретации означает, что= ∀x1 ∀x2 . . . ∀xr−1 Xfx(x1 ,x2 ,...,xr−1 )существует такая оценка ϑ = xc 1 xc 2 .. .. ..

xc r−1 , что формула ∃xr Xϑ ложна. Значит, формула12r−1Xϑ ложна при любой оценке переменной xr . Но тогда независимо от интерпретации символа fr)ϑ ложна. Значит, формула Fe ложна в данной интерпреформула Xϑxf r(c1 ...cr−1 ) , или (Xfx(x1 ...xr−1 )тации.интерпретации формула F истинна. Значит, для любой оценки ϑ =Пусть в некоторой= xc 1 xc 2 .. .. .. xc r−1 формула ∃xr Xϑ истинна, т.е. каждой оценке ϑ соответствует значение xr (ϑ),1 2r−1при котором формула X истинна.

Следовательно, определена функция xr (x1 , x2 , . . . , xr−1 ), которая при x1 = c1 , . . . , xr−1 = cr−1 принимает значение, равное соответствующему значению xr .Добавив к заданной интерпретации интерпретацию символа f как указанной функции, получиминтепретацию, в которой формула Fe будет истинной. IÌÃÒÓЗамечание 7.1. Не следует считать, что скулемовская стандартная форма данной формулыэквивалентна этой формуле. Речь идет лишь о том, что тождественная ложность (т.е.

в любой интерпретации) исходной формулы равносильна тождественной ложности ее скулемовскойстандартной формы. Рассмотрим простейший пример F = ∃xp(x). Скулемовской стандартнойформой будет Fs = p(a). Выбрав носитель интерпретации {1, 2} и положив |p(1)| = 0, |p(2)| = 1,заключаем, что формула F будет истинной. Выбрав в качестве интерпретации константы aэлемент 1, приходим к выводу, что Fs будет ложной. Значит F 6≡ Fs .Скулемовская форма не сохраняет даже свойство формулы быть тавтологией. Например,формула ∃x1 ∃x2 (p(x1 ) ∨ ¬p(x2 )) является тавтологией, в то время как ее скулемовская форма (p(c1 ) ∨ ¬p(c2 ) при определенной интерпретации предикатного символа p и констант c1 , c2оказывается ложной.

#ÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ИУ-9, МЛТА, 2009-10уч.г.ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓ72ÔÍ-12ÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓСтавится задача построения процедуры, которая за конечное число шагов даст доказательство истинности конкретной формулы. Подход, основанный на построении таблиц истинности,который работает в исчислении высказываний, в исчислении предикатов неприемлем. Нодоказательство того, что любая непротиворечивая теория интерпретируема, дает идею дляавтоматического поиска доказательства.

Отметим, что речь не идет о построении вывода втой или иной формальной системе, а лишь о проверке того, что данная формула есть тавтология. Точнее, речь идет не о проверке, а построении некоей процедуры, которая подтвердит,что данная формула есть тавтология, если это действительно так.Оказывается такую процедуру формирует синтаксический разбор, проведенный в доказательстве теоремы о непротиворечивой теории. Отметим, что задача доказать тавтологичностьформулы равносильна задаче доказать, что отрицание данной формулы является противоречием.