Файл: В. Ф. Пономарев математическая логика.doc

старше атома P_i в упорядоченном дизъюнкте тогда и только тогда, когда j > i. Например, в упорядоченном дизъюнкте (P₁P₂P₃P₄) младшим считается атом P₁, а старшим - P₄. При наличии в упорядоченном дизюънкте двух одинаковых атомов, по закону идемпотенции, следует удалить старший атом, сохранив на прежнем месте младший.

Другим усилением принципа резолюции является использование информации о резольвируемых атомах. Обычно при выполнении процедуры унификации происходит удаление резольвируемых атомов. Од­нако они несут полезную информацию. Поэтому вмес­то удаления резольвируемых атомов при унификации предлагается удалять только старший атом, а младший - сохранить в резольвенте, выделив какой-либо рамкой. Если за обрамленным атомом в резольвенте не следует никакой другой атом, то обрамленный атом удалить. Если за обрамленным атомом резольвенты следует какой-либо необрамленный атом, то его следует оставить для последующего исследования. И наконец, если последний необрамленный атом резольвенты унифицируется с отрицанием атома боковой ветви, то его следует обрамить и удалить вместе с литерой боковой ветви. Используя резольвенты на последующих этапах, можно получить обрамленными все атомы последней резольвенты, т.е.получить пустой дизъюнкт.

Пример: Суждение “Преподаватели принимали зачеты у всех студентов, не являющихся отличниками. Некоторые аспиранты и студенты сдавали зачеты только аспирантам. Ни один из аспирантов не был отличником. Следавательно, некоторые преподаватели были аспирантами.” [1] Пусть P₁(x):=”x – отличник”, P₂(x):=”x – аспирант”, P₃(x):=”x –студент”, P²₄ (x; y):=”x сдает зачет y”, P₅(x):=”x – преподаватель”. Формулы этого суждение имеют вид:

_x(P₃(x)P₁ (x)_y(P₅(y)P²₄ (x; y))); _x(P₂(x)P₃(x)_y(P²₄ (x; y)P₂ (y)));

_x(P₂(x)P₁(x)) .

 _x(P₅(x)P₂(x)).

• 
  Преобразовать посылки и отрицание заключения в ССФ:
  

1) F₁=_x(P₃(x)P₁ (x)_y(P₅(y)P²₄ (x; y)))=

---

_x_y(P₃(x)P₁ (x)(P₅(y)P²₄ (x; y)))=

_x(P₃(x)P₁ (x)(P₅(f(x))P²₄ (x; f(x)))).

M₁=(P₃(x)P₁ (x)P₅(f(x))P²₄ (x; f(x)))=

(P₃(x)P₁ (x)) P₅(f(x))P²₄ (x; f(x)) =

(P₃(x)P₁ (x) P₅ (f(x))P²₄ (x; f(x))=

(P₃(x)P₁ (x) P₅(f(x)))(P₃(x)P₁ (x) P²₄ (x; f(x))).

2) F₂=_x(P₂(x)P₃(x)_y(P²₄ (x; y)P₂ (y)))=

_x_y(P₂(x)P₃(x)(P²₄ (x; y)P₂ (y)))=

_y(P₂(a)P₃(a)(P²₄ (a; y)P₂ (y))).

M₂=(P₂(a)P₃(a)(P²₄ (a; y)P₂ (y)))=

P₂(a)P₃(a)(P²₄ (a; y)P₂ (y))).

3) F₃=_x(P₂(x)P₁(x)).

M₃=(P₂(x)P₁(x))= (P₂(x)P₁(x)).

4) F₄=_x(P₅(x)P₂(x))= _x( (P₅(x)P₂(x))).

M₄=( (P₅(x)P₂(x)))= (P₅(x) P₂(x))).

• 
  Выписать множество дизъюнктов:
  

---

K= {(P₃(x)P₁ (x)P₅(f(x))); (P₃(x)P₁ (x) P²₄ (x; f(x))); P₂(a); P₃(a);

(P²₄ (a; y)P₂(y)); (P₁(x)P₂(x)); (P₅(x)P₂(x))};

• 
  Выполнить унификацию и формирование резольвент
  

1
P₂(a)
) _x^a (P₁(x)P₂(x))  P₂(a)= P₁(a) = P₁(a);

2
P₁(a)
)P₁(a)_x^a(P₃(x)P₁ (x)P²₄ (x; f(x)))= P₃(a) P²₄ (a; f(a));

3
P₁(a) ₁(a)
) P₃(a)  P²₄ (a; f(a)) _y^f(a) (P²₄ (a; y)P₂(y))=


P₁(a)

P²₄ (a; f(a))
P₃(a)  P₂(f(a));


P₁(a)

P²₄ (a; f(a))
4) P₃(a)  P₂(f(a)) _x^f(a)(P₅(x)P₂(x))=


P₁(a)

P²₄ (a; f(a))

P₂(f(a))
P₃(a)  P₅(f(a));


P₁(a)

P²₄ (a; f(a))

P₂(f(a))
5) P₃(a)  P₅(f(a)) 

_x
P₁(a)

P₅(f(a))

P₂(f(a))

P²₄ (a; f(a))
^a(P₃(x)P₁ (x)P₅(f(x)))= P₃(a)     P₁ (a);


P₁(a)

P²₄ (a; f(a))

P₂(f(a))

P₅(f(a))
6) P₃(a)    P₁ (a)P₁(a)=


P₁(a)

P₁(a)

P²₄ (a; f(a))

P₂(f(a))

P₅(f(a))
P₃(a)    =


P₁(a)
P₃(a);


P₁(a)

P₁(a)

P₃(a)
7) P₃(a)  P₃(a)=  = .
На рис. 14 дан граф линейной унификации этого примера.
P₁(x)P₂(x)

P₁(a) P₂(a)


P₁(a)
P₃(a) P²₄ (a; f(a)) P₃(x)P₁ (x)P²₄ (x; f(x))


P²₄

---

(a; f(a))

P₁(a)
P₃(a)  P₂(f(a)) P²₄ (a; y)P₂(y)


P₁(a)

P²₄ (a; f(a))

P₂(f(a))
P₃(a)    P₅(x)P₂(x)


P₂(f(a))

P²₄ (a; f(a))

P₁(a)
P₅(f(a))

P₃(a)   P₃(x)P₁ (x)P₅(f(x))


P₁(a)

P₅(f(a))
 P₁ (x)

P₃(a) P₁(a)

• 
  P₃(a)
  

Рис. 14. Граф линейной унификации
Пример: Существуют студенты, которые любят всех преподавателей. Ни один из студентов не любит невежд. Следовательно, ни один из преподавателей не является невеждой. [1]

Пусть P₁(x):=” x – студент”, P₂(y):=”y – преподаватель”, P²₃(x, y):=”x любит y”, P₄(y):=”y - невежда”.

Формулы этого суждение имеют вид:

_x(P₁(x)_y(P₂ (y)P²₃(x; y)));

 _x(P₁(x) _y(P₄ (y)P²₃(x; y)));

_y(P₂ (y)P₄(y));

• 
  Преобразовать посылки и отрицание заключения в ССФ:
  

1. 
   F₁=_x(P₁(x)_y(P₂ (y)P²₃(x; y)))= _x_y(P₁(x) (P₂ (y)P²₃(x; y)))= _y(P₁(a) (P₂ (y)P²₃(a; y)))= _y(P₁(a) (P₂ (y)P²₃(a; y)));
   

M₁= P₁(a)(P₂ (y)P²₃(a; y));

2. 
   F₂=_x(P₁(x) _y(P₄ (y)P²₃(x; y)))=
   

_x_y (P₁(x)  (P₄ (y)P²₃(x; y)))= _x_y (P₁(x)P₄ (y)P²₃(x; y)));

M₂=(P₁(x)P₄ (y)P²₃(x; y));

3. 
   F3=_y(P₂ (y)P₄(y))= _y((P₂(y)P₄(y))= _y(P₂(y) P₄(y))=
   

P₂(b)P₄(b);

M₃=P₂(b)P₄(b).

• 
  Выписать множество дизъюнктов:
  

K={P₁(a); (P₂ (y)P²₃(a; y)); (P₁(x)P₄ (y)P²₃(x; y)); P₂(b); P₄(b)};

---

• 
  Выполнить унификацию и формирование резольвент:
  

P₂(b)
1) P₂(b)  _x^b(P₂ (y)P²₃(a; y))= P²₃(a; b);


P₂(b)
2) P²₃(a; b)_y^b (P₁(x)P₄ (y)P²₃(x; y))=


P₂(b)
P²₃(a; b)(P₁(x)P₄ (b)P²₃(x; b));

3
P₂(b)
) P²₃(a; b)_x^a(P₁(x)P₄ (b)P²₃(x; b))=

• 
  
  P₂(b)
  
  P²₃(a; b)
  P₁(a)P₄ (b);
  

4
P₂(b)

P²₃(a; b)
)  P₁(a)P₄ (b) P₁(a)=


P₂(b)

P²₃(a; b)

P₁(a)
  P₄ (b);

5
P₂(b)

P²₃(a; b)

P₁(a)
)   P₄ (b) P₄(b)=


P₂(b)

P²₃(a; b)

P₁(a)

P₄ (b)
  = .
На рис. 15 приведен граф линейной унификации для этого примера.

P₂(b)


P₂(b)

P₂(b)
P²₃(a; b) P₂ (y)P²₃(a; y)

P²₃(a; b) (P₁(x)P₄ (b) P₁(x)P₄ (y)P²₃(x; y)


P₂(b)
P²₃(x; b))


P²₃(a; b)

P₁(a)
 P₁(a) P₄ (b) P₁(x)P₄ (b)P²₃(x; b))


P₂(b)

P²₃(a; b)
  P₄ (b) P₁(a)

 P₄(b)

Рис. 15. Граф линейной унификации
2.3 Проблемы в исчислении предикатов

Для обоснования исчисления предикатов, как для любой аксиоматической теории, необходимо рассмотреть проблемы разрешимости и непротиворечивости.

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

---