Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

R - ((Di )в - (Li)g) v((D2)e - (L2)e) называется бинарной резольвентой Dj и (в логике предикатов). Литеры L ih L 2 называются отрезаемыми литерами. Рассмотрим пример. Пусть Di=P(x) vQ(x), D2 = -nP(a)vT(x). Переименуем X в D2: D2 = -пР(а) vT(y). Положим, что в = {а/х}. Тогда имеем (Di)e = Р(а) vQ(a) , (D2)e = -^(а) vT(y) , Отбрасываем литеры Р (а), —Р (а) и получим бинарную резольвенту: R =Q (а) vT (у). Пусть имеем 1)7= -^(х) vQ(x), D2 = -^Q(x) vT(x). Тогда = -^Q(y) vT(y) = ^ (у) vT(y). Резольвентой дизъюнктов - посылок Di я D2 называется одна из следую­ щих бинарных резольвент: 1) бинарная резольвента Dj ж D2, 2) бинарная резольвента Dj и склейки D2, 3) бинарная резольвента D2 и склейки Di, 4) бинарная резольвента склейки Di и склейки Z)^. Методом резолюций в логике предикатов считается последовательное по­ лучение резольвент из заданного множества дизъюнктов и вновь получаемых дизъюнктов. Можно доказать следующую важную теорему. Теорема 3.10 (полнота метода резолюций). Множество S дизъюнктов не­ выполнимо тогда и только тогда, когда существует вывод пустого дизъюнкта из S. Проблема дедукции логики предикатов состоит, как и в логике высказыва­ ний, в выяснении: будет ли формула В логическим следствием формул Aj, А2, , Afi. Теоремы 3.1-3.4, доказанные для логики высказываний, можно распро­ странить и для логики предикатов, записывая всюду вместо слова «тавтология» слова «логически общезначимая формула». Из изложенного можно получить следующую последовательность дейст­ вий для выяснения будет ли замкнутая формула В логическим следствием замкнутых формулЛ 7, Л 2, ...,Ап. 1. Строим конъюнкцию С= A1&A2& ... & A „.&—iB. Отметим, что требуемое следствие (заключение) взято с отрицанием. 2. Паходим (сколемовскую) стандартную форму Cs для формулы С. Поло­ жим, что форма Cs = (QiXiQ2X2...QnXr)'Ci&C2&...&Cn, где =(QiXiQ2X2...QnXn) - префикс формулы без кванторов существования, а Ci,C2, ..., € „ - элементарные суммы, в которых по необходимости введены сколемовские функции. Элемен- 77