2.2. Логика предикатов первого порядка

2.2.1. Основные определения.
Как показывает практика, возможностей логики высказываний явно недостаточно для представления знаний. Напомним основные понятия более сложной логики предикатов первого порядка (ЛППП).
Предикат – это логическая функция одного или нескольких переменных. Результатом этой функции является 1 – истина или 0 – ложь.
Примеры. СТУДЕНТ (Вася), ПРОЖИВАНИЕ (x, Томск).
Терм – это константа, переменная или некоторая n-местная функция (функтор f(x1,…,xn))
Примеры. а  ,  x,  f(x, y).
Если P – n-местный предикат и t1…tn – термы, то P(t1,…,tn) – атом.
Примеры. P(x), P(x,y), P(a, x), P(x, y, f(x, y)).
В формулах используются логические связки (операции):ù, Ù, Ú, ®, « и кванторы:", $.
Рекуррентное определение формулы:

• Атом – есть формула
• Если F – формула, то ùF – формула.
• Если F, G – формулы, то FÚG, FÙG, F®G, F«G – формулы.
• Если F – формула, в которой есть переменная x, то "x F(x), $x F(x) – формулы (при этом переменная x называется связанной квантором всеобщности или существования).
• Все переменные в формуле связаны кванторами.

Пример. Формализуем утверждение: «для любого натурального числа существует единственное натуральное число, непосредственно следующее за ним».
Введем предикаты E(x, y) – x=y, N(x) – x – натуральное число и функтор f(x) –  следующее число (x+1).
"x [N(x)®$y [E(f(x), y)Ù"z [E(f(x), z)®E(y, z)]]].
Интерпретация формул производится следующим образом:
А) Считаем, что для каждой формулы определено множество объектов, о которых может идти речь, это множество называется областью определения формулы (обозначается D).

• Каждой константе ставим в соответствие один элемент из D.
• Определяем значения функций для всех возможных наборов аргументов.
• Определяем истинностное значение каждого предиката.
• Устанавливаем истинностное значение формулы по таблицам истинности (это можно сделать только в случае, если все переменные в формуле связаны кванторами – иначе, формула бессмысленна)

Пример.
"x [P(x)→Q(x,f(x))]
A) D = {1, 2} – область определения
B) Константы отсутствуют
С) f  (1) = 2                 f (2) = 1
D) P (1) = 1                 P (2) = 0
Q (1, 1) = 1             Q (1, 2) = 0              Q (2, 1) = 0           Q (2, 2) = 1
E) Вычисляем значение матрицы
x = 1
P (x) → Q (x, f (x)) = P (1) → Q (1, f(1)) = P(1) → Q (1, 2) =1 → 0 = 0
Таким образом:
"x [P(x) → Q (x, f(x))] = 0 в данной интерпретации.
В этой же интерпретации формула
$x [P(x) → Q (x, f(x))] = 1,
т.к.
при x = 2
P(x) → Q (x, f(x) = P(2) → Q (2, f (2)) = 0 → 0 = 1              

      
Определения общезначимости, противоречивости и логического следствия точно соответствуют аналогичным понятиям в логике высказываний. Имеют место те же теоремы дедукции. Справедливыми остаются и эквивалентные преобразования.
Для того чтобы формулы привести к виду, с которым удобно работать производят их стандартизацию.
А) Избавляются от операций ®, « с помощью соответствующих правил (см. 2.1.1).
B) Добиваются, чтобы ù стояло только перед атомом (используем законы Де Моргана см. 2.1.1)
С) Переносят кванторы в начало формулы, чтобы она имела вид:
1 x1 2 x2 ….. n x n       M [x1,  … , xn] 
В этом случае говорят, что формула представлена в ПНФ (предваренной норм форме). M[x1,…,xn]  называется матрицей формулы.
Используются следующие эквивалентные преобразования:
 x F(x) G =  x [F(x) G]
в случае, если G не содержит переменную x:
1 x F (x)  2x G(x) = 1 x  2 y [F1(x) G2(y)],
т.е. в случае необходимости производим замену переменных.
В двух частных случаях можно избежать переименования переменной:
"x F (x) Ù "x G(x) = "x [F(x) Ù G(x)]
$ x F(x) Ú $ x G (x) = $ x [F(x) Ú G(x)]
D) Добиваются, чтобы матрица была представлена в КНФ.
E) Избавляются от $ путем замены связанных им переменных на константы.
F =  x1 …  xi-1 $ xi  xi+1 …  xn M [x1 …, xi-1, xi ; xi+1; xn]
G =  x1 …  xi-1 …   xi+1 …  xn M [x1, …, xi-1, a, xi+1, … xn],
где :
а – некоторая константа.
Таким образом, заменяем переменные под $ на константы.
Это преобразование не является эквивалентным, однако оно сохраняет противоречивость, т.е. F- противоречива, тогда и только тогда, когда противоречива G. Этого достаточно, если мы пользуемся 2-й теоремой дедукции.

2.2.2. Метод резолюции в ЛППП.
Литеры  L1 и L2 называются контрарными, если они являются отрицанием друг друга c точностью до унификации (то есть одна из литер изначально является отрицанием другой или ее можно таковой сделать с помощью подстановки).
Примечание. Формальное определение подстановки будет приведено ниже.
Бинарной резольвентой клозов С1 и С2, содержащих контрарные литеры L1 и L2 назовается клоз C, полученный следующим образом:
С={C1\L1}È{C2\L2}
Примечание. Очевидно, что данное определение аналогично соответствующему определению в логике высказываний.

Примеры.

P (x) Ú Q (x, y) ù P(x) Ú R(z) Q(x,  y) Ú R (z)

P (x) Ú Q (x, y) ù P(a) Ú  R (z) {a/x} Q(a, y) R (z)

Доказано, что бинарная резольвента является логическим следствием.
В отличии от ЛВ, в ЛППП различают понятия резольвенты и бинарной резольвенты. Для того, чтобы определить понятие резольвенты необходимо рассмотреть подстановки.
Множество вида {ti/xi, … tn/xn}, где ti – термы, а xi – переменные называется подстановкой термов ti вместо переменных xi.
Если E – клоз, а Θ – подстановка, то EΘ – подстановочный частный случай, получаемый вследствие замены переменных xi на термы ti.
Пример.
P (x) Ú Q (f (x), b, y)
{a/x, c/y}
P (a) Ú Q (f (a), b, c)
Примечание. Подстановка действительно приводит к переходу от более общего случая к частному и таким образом обеспечивает сохранение противоречивости.
Пусть даны 2 подстановки Θ и Ω. Применим подстановку Θ, а затем подстановку Ω. Тогда будем говорить, что применили композицию подстановок ΩΘ.
Подстановка Θ называется  унификатором множества выражений {E1,..,En}, если E1Θ =E2Θ =….=EnΘ.
Подстановка Ω - есть наиболее общий унификатор множества  выражений {E1,…,Ek}, если любой унификатор это множества выражений Θ можно получить путем композиции Ω с некоторой подстановкой Ψ. (Θ= ΩΨ).
П. С – дизъюнкт, а Θ - наиболее общий унификатор двух и более его литер, тогда СΘ называется склейкой дизъюнкта С.
Пример.
P (x) Ú Q (f(x), b, y) Ú P (a)
{a/x)
P (a) Ú Q (f(x), b, y)
Резольвентами дизъюнктов С1 и С2, содержащих контрарные литеры L1 и L2 называются бинарные резольвенты:

• клозов С1 и С2;
• любой склейки клоза C1 и клоза С2;
• клоза С1 и любой склейки клоза С2;
• любых склеек клоза С1 и С2

Последовательность получения резольвент из множества клозов, в результате которой получают пустой клоз, называется резолютивным выводом в ЛППП.
Примечание. Фактически, вывод сводится к последовательности вычисления бинарных резольвент и склеек.
Пример.
Аксиома 1. Мао Цзедун – человек
Аксиома 2. Все люди смертны.
Теорема. Мао Цзедун – смертен.
Вводим предикаты:
C (x) – x - человек
S (x) – x -  смертен
Аксиома 1             C (Мао)
Аксиома 2             [C (x) → S (x)] =
Теорема                  S (Мао)

С (Мао)                                                       S (Мао)
ù С (x) Ú S (x)             {Мао / x}            
S (Мао)                                                        ù S (Мао)

Здесь также справедлива теорема о полноте резолютивного вывода. Множество клозов S противоречиво, если и только если существует резолютивный вывод пустого клоза из S.
Очевидно, что для того чтобы проверить противоречиво ли множество клозов, следует перебрать множество попыток провести резолюции. Таким образом, строится дерево резолюций. Способ построения такого дерева фактически является  стратегией проведения резолюции.
Формальный алгоритм незначительно отличается от имеющегося в ЛВ.
ВХОД: S – входное множество клозов.
ВЫХОД: OK – удается получить пустой клоз, NO – не удается.
M:=S; // - M-текущее множество клозов.
while      ÏM do
if not Choose (M, C1, C2, p1, p2) then return(NO);
N:=R(M, C1, C2, p1, p2); // - вычисление резольвенты.
M:=M È N; // - пополнение текущего множества.
end
return (OK); //получен пустой клоз
Примечание. Результат функции R здесь множество возможных резольвент клозов С1 и С2, содержащих контрарные литеры р1 и р2.

2.2.3. Стратегии проведения резолюции.
В настоящее время предложено множество различных стратегий резолюций. Как уже отмечалось, различают полные и неполные стратегии. Полные стратегии гарантируют вывод пустого клоза на противоречивом входном множестве.
Рассмотрим самые распространенные стратегии.

1. Полный перебор. Проверяются все возможные варианты поиска резольвент на каждом шаге. Недостаток этой стратегии заключается в том, что очень высока трудоёмкость соответствующего алгоритма. Основное достоинство – полнота.
2. Линейные резолюции. Линейным называется вывод, удовлетворяющий следующей схеме (рис 2.1):

Рис 2.1. Схема линейной резолюции

где Сi - центральные клозы, Вj - боковые. Боковой клоз всегда выбирается либо из входного множества (S), либо среди клозов, полученных на предыдущих шагах. Клоз C называется верхним в выводе. Под входным понимается само начальное множество опровергаемых клозов.
Bj   S    или     Bj = Ci ,
где:  i < j
Недостаток этой стратегии в том, что  она не полная.

1. Входная резолюция.

Это частный случай линейной резолюции. Накладывается дополнительное условие на то, что боковой клоз можно выбирать только из входного множества. Сохраняется основной недостаток линейной резолюции, заключающийся в ее неполноте.
B;  S

1. Стратегия OL-вывода (Ordered Lined).
2. Вывод на клозах Хорна (реализован  в Прологе).

Примечание. Последние две стратегии будут рассмотрены подробнее, как наиболее часто применяющиеся на практике.