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

Здесь P — некотораяэлементарная формула.Однако только такого склеивания дизъюнктов недостаточно. Отметим, что нашей цельюявляется установление противоречивости множества дизъюнктов. С этой целью мы довольносвободно можем менять переменные в аргументах предикатных символов данной формулы.Реализуется это механизмом подстановки. Идея такова: подобрать такую подстановку, чтоэлементарные формулы, содержащие данный предикатный символ, преобразовались в одну иту же формулу. Подстановка не нарушает условия противоречивости (или тавтологичности).Пусть дано множество формул Φ1 , Φ2 ,.

. . , Φk . Подстановка ϑ называется унификаторомэтого множества, если Φ1 ϑ = Φ2 ϑ = . . . = Φk ϑ. Если множество имеет унификатор, то ононазывается унифицируемым.yПример 7.4. Множество {p(a, y), p(x, f (b))} имеет унификатор x. Следовательно,a f (b)ÔÍ-12ÔÍ-127.3. Метод резолюций для исчисления предикатовÌÃÒÓÌÃÒÓe 1 ∨ xn , а D2 имеет вид D2 = De 2 ∨ ¬xn . Резольвента D двух дизъюнктов, имеющая видD1 = DeeD = D1 ∨ D2 , противоречива и в L1 , и в L2 . Удаляем листья L1 , L2 , а порождающему их узлуставим в соответствие резольвенту.Продолжая процедуру отрезания пар листьев, мы последовательно сокращаем размер дерева,причем на каждом шаге каждому листу соответствует дизъюнкт, являющийся противоречивымпри соответствующих значениях переменных.

В этот дизъюнкт входят только те переменные,которые однозначно определяются узлом исходного дерева. Отрезав все листья, получим деревоиз одного корня, которому соответствует пустой дизъюнкт. IÌÃÒÓÔÍ-12ÌÃÒÓ75ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓ7. Метод резолюцийÔÍ-12ÌÃÒÓменная x, а второй есть терм T . Во всех формулах выполняем подстановку Tx . Процедуруповторяем. Если в какой-то момент очередной список рассогласования не имеет переменных, томножество формул не унифицируемо. Другой вариант завершения процедуры — пустой списокрассогласования (формулы стали одинаковыми). Тогда множество унифицируемо, а наиболееобщий унификатор — композиция всех выполненных подстановок.те получим множество p(a, x, f (g(y))), p(a, f (a), f (u)).

Следующий список рассогласованийx. Реализация этой подстановки дает множество{x, f (a)} устраняется подстановкой f (a)2. Рассмотрим множество q(f (a), g(x)), q(y, y). Первый список рассогласования {f (a), y}yустраняется подстановкой f (a) . В результате реализации этой подстановки получим множество q(f (a), g(x)), q(f (a), f (a)). Второй список рассогласования {g(x), f (a)} не может бытьустранен, поскольку среди термов нет ни одной переменной. Вывод: рассматриваемое множество не унифицируемо.ÔÍ-12p(a, f (a), f (g(y))), p(a, f (a), f (u)). Следующий список рассогласований {g(y), u}.

Устраняющаяuподстановка g(y) . Реализуем ее: p(a, f (a), f (g(y))), p(a, f (a), f (g(y))). Получили одинаковыеz xuформулы. процесс унификации закончен. Унификатор: a f (a) g(y) .ÌÃÒÓПример 7.7. 1. Рассмотрим множество из двух формул p(a, x, f (g(y))), p(z, f (z), f (u)).

Первый список рассогласований: {a, z}. Он устраняется подстановкой az . В результа-ÔÍ-12Рассмотрим некоторое множество элементарных формул p(T1j , T2j , . . . , Tkj ), j = 1, 2, . . . , s.Находим список рассогласования и в нем определяем два терма, один из которых есть пере-ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12Пример 7.6. В множестве формул p(x, f (y, z)), p(x, a), p(x, g(h(k(x)))) различие начинаетсяс позиции 5. С этой позиции в первой формуле начинается терм f (y, z), во второй — терм a,в третьей — терм g(h(k(x))).

Рассогласование в данном случае — список термов f (y, z), a,g(h(k(x))).Рассмотрим множество формул p(x, f (y, z)), p(x, f (g(x), z)), p(x, f (a, x)). В данном случаеформулы имеют одинаковый первый аргумент, а второй у них различается. Но при этом у ниху всех этот аргумент порожден одним и тем же функциональным символом f . Различие порсимволам наступает в позиции 7, в которой начинается первый аргумент символа f . Выписываяпо всем формулам эти аргументы, получаем рассогласование y, g(x), a.ÃÒÓÌÃÒÓАлгоритм, позволяющий для любого конечного множества элементарных формул с одинаковым предикатным символом построить наиболее общий унификатор или доказать, что этомножество не унифицируемо, довольно прост. Его идея заключается в том, чтобы найти рассогласования в формулах, а потом найти подстановку, которая это рассогласование устраняет(ну, или убедиться в том, что это рассогласование неустранимо).

Например, в формулах p(x, b)и p(a, b) рассогласование заключается в том, что на местах, в которых в первой формуле находится переменная x, вторая формула содержит константу a. Рассогласование можно устранитьподстановкой вместо x константы a.Рассматриваем множество элементарных формул вида p(T1 , T2 , . . . , Tn ) с одинаковым предикатным символом. У таких формул последовательности аргументов имеют одинаковую длинуи одинаковые последовательности сортов.

Мы сравниваем у всех формул первые аргументы,затем вторые и т.д., пока не найдем очередную серию аргументов, в которой есть неодинаковыетермы. Эти термы могут порождаться одним и тем же функциональным символом. Тогда мыпереходим к сравнению аргументов этого функционального символа. Происходит анализ всегосинтаксического дерева. Формально это можно провести так. Просматриваем формулы как последовательности символов слева направо до появления на очередной позиции разных символов.В каждой формуле с этой позиции начинается некоторый подтерм. Список таких подтермов иесть список рассогласования.ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ИУ-9, МЛТА, 2009-10уч.г.ÔÍ-12ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓ76ÌÃÒÓÔÍ-12ÌÃÒÓ77Пусть в дизъюнкте C несколько литер L1 , L2 , .

. . , Lk с предикатным символом p однойполярности (т.е. либо все с отрицанием, либо все без отрицания). Предположим, что они имеютнаиболее общий унификатор ϑ. Тогда формулы L1 ϑ, L2 ϑ, . . . , Lk ϑ совпадают и в дизъюнкте Cϑзаменяются одной литерой. Дизъюнкт Cϑ в этом случае называется склейкой дизъюнкта C.Пусть C1 и C2 — два дизъюнкта, не имеющих одинаковых переменных. Предположим, что вних входят литеры вида p(. .

.) и ¬p(. . .), для которых существует наиболее общий унификаторe1 , C2 = ¬p(. . .) ∨ Ce2 . После подстановки заменим литеры pϑ, т.е., например, C1 = p(. . .) ∨ Cсовпадут, и мы можем сформировать резольвенту C1 ϑ ∨ C2 ϑ, которая называется бинарнойрезольвентой C1 и C2 .Мы рассматриваем множество дизъюнктов как скелет“ матрицы скулемовской стандартной”формы. Значит, в действительности все переменные связаны кванторами всеобщности. Ноотметим, чтоÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓ7. Метод резолюцийÔÍ-12Требуется опровержение формулы F1 ∧ F2 ∧ ¬G, которая имеет скулемовскую формуF1 ∧ F2 ∧ ¬G ' ∀x [¬c(x) ∨ w(x)] ∧ [¬c(x) ∨ r(x)] ∧ c(a) ∧ q(a) ∧ [¬q(x) ∨ ¬r(x)] .¬c(x) ∨ w(x),¬c(x) ∨ r(x),c(a),q(a),ÌÃÒÓОтбрасывая квантор, получим множество дизъюнктов¬q(x) ∨ ¬r(x).Для доказательства противоречивости этого множества используем метод резолюций:¬c(x) ∨ r(x)c(a)¬q(x) ∨ ¬r(x)q(a)Поскольку методом резолююций получен вывод пустого дизъюнкта, заключаем, что множество дизъюнктов противоречиво, а следовательно, формула G есть логическое следствие F1и F2 .ÔÍ-12¬r(a)r(a)ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12Пример 7.9.

Рассмотрим формулы F1 = ∀x(c(x) → w(x) ∧ r(x)); F2 = ∃x(c(x) ∧ q(x));G = ∃x(q(x) ∧ r(x)). Покажем, что G есть логическое следствие F1 и F2 . Это значит, чтомножество формул F1 , F2 , ¬G противоречиво.Преобразуем формулы рассматриваемого множества в скулемовскую стандартную форму:F1 ' ∀x(¬c(x) ∨ (w(x) ∧ r(x)) ' ∀x [¬c(x) ∨ w(x)] ∧ [¬c(x) ∨ r(x)] ;F2 ' c(a) ∧ q(a);¬G ' ∀x(¬q(x) ∨ ¬r(x)).ÔÍ-12ÌÃÒÓПример 7.8. В множестве формул ¬p(x, y), p(a, b)∨p(a, z)∨p(f (x), f (x)) во втором дизъюнкте возможна склейка второй литеры с первой, а третья литера не слеивается ни с чем. Послесклейки получим формулу p(a, b) ∨ p(f (x), f (x)), которая имеет резольвенту с первой формулойp(f (a), f (a)).ÌÃÒÓÔÍ-12Это показывает, что скулемовскую стандартную форму можно составить так, что во всех еедизъюнктах будут разные переменные.Резольвентой двух дизъюнктов C1 , C2 называется бинарная резольвента C1 или его склейки и C2 или его склейки.

Здесь четыре ситуации: дизъюнкт–дизъюнкт, склейка–дизъюнкт,дизъюнкт–склейка и склейка–склейка.ÔÍ-12ÔÍ-12∀x(D1 (x) ∧ D2 (x)) ≡ ∀xD1 (x) ∧ ∀xD2 (x) ≡ ∀x1 D1 (x1 ) ∧ ∀x2 D2 (x2 ) ≡ ∀x1 ∀x2 (D1 (x1 ) ∧ D2 (x2 )).ÌÃÒÓÌÃÒÓÔÍ-12ИУ-9, МЛТА, 2009-10уч.г.Пример 7.10.

Рассмотрим формулыF1 = ∃x p(x) ∧ ∀y[d(y) → r(x, y)] , F2 = ∀x p(x) → ∀y[q(y) → ¬r(x, y)] ,G = ∀x[d(x) → ¬q(x)].Выясним, является ли формула G логическим следствием F1 и F2 .Приведем формулы к скулемовской стандартной форме. Для формулы F1 имеем:F1 ≡ ∃x∀y p(x) ∧ [d(y) → r(x, y)] ≡ ∃x∀y p(x) ∧ [¬d(y) ∨ r(x, y)] ' ∀y p(a) ∧ [¬d(y) ∨ r(a, y)] .ÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓ78Для формулы F2 получаемF2 ≡ ∀x∀y p(x) → [q(y) → ¬r(x, y)] ≡ ∀x∀y ¬p(x) ∨ ¬q(y) ∨ ¬r(x, y) .Наконец, преобразуем отрицание формулы G:В результате получаем следующее множество дизъюнктов:p(a),¬d(y) ∨ r(a, y),¬p(x) ∨ ¬q(y) ∨ ¬r(x, y),d(b),q(b).Приведем дерево резольвентного вывода:¬p(x) ∨ ¬q(y) ∨ ¬r(x, y)¬q(y) ∨ ¬r(a, y)ÌÃÒÓÌÃÒÓp(a)¬d(y) ∨ r(a, y)¬q(y) ∨ ¬d(y)q(b)¬d(b)d(b)ÌÃÒÓÌÃÒÓÔÍ-12В результате множество дизъюнктов противоречиво, т.е. формула F1 ∧ F2 → G является тавтологией, а формула G есть логическое следствие F1 и F2 .ÔÍ-12ÔÍ-12ÔÍ-12ÔÍ-12¬G ≡ ∃x¬[d(x) → ¬q(x)] ≡ ∃x¬[¬d(x) ∨ ¬q(x)] ≡ ∃x[d(x) ∧ q(x)] ' d(b) ∧ q(b).ÔÍ-12ÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÌÃÒÓ151517223.

Алгебра предикатов3.1. Предикаты и кванторы . . . . . . . . . . .3.2. Логико-математические языки . . . . . . .3.3. Переименования и подстановки . . . . . .3.4. Семантика логико-математического языка3.5. Логические законы . . . . . . . . . . . . .3.6. Замены . . . . . . . . . . . . . . . . . . . .3.7. Упрощение формул . . . . . . . . . .

. . ........27272831343639414. Исчисление предикатов4.1. Построение теории P . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4.2. Правила естественного вывода . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4.3. Глобальные свойства теории P . . . . . .