Специальная математика. Соловьев А.Е. - 35 стр.

  Где Миша?                                А3. х B(M, x) ?
  Вопрос (доказываемую формулу с добавленным знаком вопроса) х B(M, x)?
  преобразуем в .¬ х B(M, x) (отрицание вопроса). Далее
  задвигаем отрицание за квантор, производим сколемизацию и
  добавляем специальный «предикат ответа», который будет аккумулировать процесс
унификации). В результате получаем дизъюнкт:
  .¬ B(M, x)  Отв(М, x)
  Вся система (две аксиомы и вопрос) будет состоять из трех дизъюнктов:
  Д1: ¬B(Л, x)  B(M, x)
  Д2:B(Л, Ш)
  Д3: ¬B(M, x)  Отв(M, x)

   Вывод:
   Резолюция Д1-Д2 дает Д4: B(M,Ш)
   Резолюция Д4-Д3 дает Д5: Отв(M,Ш)
   То есть. предикат ответа (при получении пустого дизъюнкта) можно интерпретировать
как «Миша в школе».(Интерпретация ответа в системе искусственного интеллекта остается
за человеком).

   Пример 2:
1. Если х является родителем y и y является родителем z, то х является прародителем
z.
А1. xyz(P(x, y) & P(y, z)  (x, z)
2. Каждый человек имеет своего родителя.
A2. yxP(x, y)
3. Существуют ли такие х и у , что х является прародителем у ?
xy(x, y) ?

   Преобразуем аксиомы в дизъюнкты.
   Д1. Р(х, у) Р(у, z)  (x, z)
   Д2. P(f(y), y)
   Д3.(x, y)  Отв(x, y)
   Д1 - Д2: Д4: Р(у, z)  ( f(y), z)
   Д4 – Д2: Д5: (f(f(y)), y)
   Д5 – Д3: Д6:  (f(f(х)), х)
   Заметим, что каждая переменная имеет уникальное имя в пределах одного дизъюнкта.
Переменные, названные одинаково в разных дизъюнктах - это разные переменные.
Интерпретация результата лежит на человеке. Будем интерпретировать
   f(х)- как быть родителем х. То есть f(f(х) - родитель родителя х. Следовательно, (f(f
(х)), х) – прародитель х - это родитель родителя х.

                                   2.6. Система Генцена

  В ее основе лежит понятие секвенции.
  Секвенции имеют вид

   антецедент - A1, A2, ... An  B1, B2, ... Bn - сукцедент

                               

                                             — 35 —