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

₅ и правилу 1 введения квантора общности.

Так доказана истинность формулы _x(P₃(x)(P₂(x))).

На рис. 12 приведен граф, иллюстрирующий процесс дедуктивного вывода.


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

_x(P₃ (x)P₁ (x))



(P₁ (t)( P₂ (t)))

P₃ (t) P₁ (t)




(P₃ (t)( P₂ (t)))



_x(P₃(x)(P₂(x)))


Рис. 12. Граф вывода заключения


Пример: Доказать истинность заключения

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

_x(P₃(x))_x_y(P²₁.(x; y)(P₂(y))).
1) F₁=_x(_y(P²₁.(x; y)P₂(y))_y((P₃(y) P²₄.(x; y))) - посылка;

2) F₂= _x(P₃(x)) -посылка;

3) F₃=_x(P₃(x)) - заключение no формуле F₂ и правилу 5) смены кванторов (закон де Моргана);

4) F₄=P₃ (t) - заключение по формуле F₃ и правилу 2) удаления квантора общности;

5) F₅=P₃(t)P²₄.(x;t) - заключение по формуле F₄ и правилу 4) исчисления высказываний;

6) F₆=_y(P₃(y)(P²₄ (x; y))) - заключение по формуле F₅ и правилу 1) введения квантора общности;

7) F₇=_y(P₃(y)P²₄ (x; y)) - заключение по формуле F₆ и правилу смены кванторов (закон де Моргана);

8) F₈=_y(P²₁.(t; y)P₂(y)y(P₃(y)P²₄.(t; y)) - заключение по формуле F₁ и правилу 2) удаления квантора общности;

9) F₉= y(P²₁.(t; y)P₂(y)) - заключение пo формулам F₇ и F₈ при условии t=x и правилу modus tollens;

10) F₁₀=_y( P²₁.(t; y)P₂(y)) - заключение по формуле F₉ и правилу смены кванторов (закон де Моргана);

11) F₁₁=_y(P²₁. (t; y) (P₂

---

(y)) - заключение пo формуле F₁₀ и эквивалентным преобразованиям алгебры предикатов;

12) F₁₂=_x_y(P²₁. (x; y) (P₂ (y)) - заключение по формуле F₁₁ и правилу 1) введения квантора общности;

13) _x(P₃(x))_x_y(P²₁.(x; y)( P₂(y))) – заключение по формулам F₂ и F₁₂ и правилу modus ponens. Что и требовалось доказать.


 _x(P₃(x))

_x(_y(P²₁.(x; y)P₂(y))_y((P₃(y) P²₄.(x; y)))
На рис. 13 приведен граф вывода этой задачи.






_x(P₃(x))

_y(P²₁.(t; y)P₂(y)_y(P₃(y)P²₄.(t; y))





P₃ (t)

 y(P²₁.(t; y)P₂(y))





P₃(t)P²₄.(x;t)

_y( P²₁.(t; y)P₂(y))





_y(P²₁. (t; y) (P₂ (y))

_y(P₃(y)(P²₄ (x; y)))





_y(P₃(y)P²₄ (x; y))

_x_y(P²₁. (x; y) (P₂ (y))


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

рис. 13 Граф вывода заключения

Пример. Доказать истинность заключения

---

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

_x(P₂(x)P₃(x)).
1) F₁=_x(P₁(x)_y(P₂(y)P²₄.(x; y))) - посылка;

2) F₂=_x(P₁(x)_y(P₃(y)P²₄ (x; y))) - посылка;

3) F₃=P₁(а)_y(P₂(y)P²₄.(a; y))-заключение по формуле F₁, правилу формирования ССФ;

4) F₄=P₁(a)- заключение по формуле F₃ и правилу удаления конъюнкции исчисления высказываний

5) F₅=_y(P₂(y) P²₄.(a; y)) - заключение пo формуле F₃ и правилу удаления конъюнкции исчисления высказываний;

6) F₆=P₂(t) P²₄.(a; t) - заключение по формуле F₅ и правилу 2) удаления квантора общности;

7) F₇=P₁(t)_y(P₃(y)P²₄ (t; y)) - заключение по формуле F₂ и правилу 2) удаления квантора общности;

8) F₈=_y(P₃(y) P²₄ (a; y)) - заключение по формулам F₃ и F₇ при t=a и правилу modus ponens;

9) F₉=P₃(t)P²₄.(a; t) - заключение по формуле F₈ и правилу 2) удаления квантора общности;

10) F₁₀=P²₄.(a; t)P₃(t) - заключение по формуле F₉ и закону контрапозиции (правило 8) исчисления высказываний);

11) F₁₁=P₂(t)P₃(t) - заключение по формулам F₆ и F₁₀ и закону силлогизма (правило 11) исчисления высказываний);

12) F₁₂=_x( P₂ (x)P₃(x)) - заключение по формуле F₁₁ и правилу 1) введения квантора _x. Что требовалось доказать.

На рис. 14 приведен граф вывода этой задачи.

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

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






x=a


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

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

---

P₁(a)

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

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









_y(P₃(y) P²₄ (a; y))

P₂(t) P²₄.(a; t)






P₃(t)P²₄.(a; t)





P²₄.(a; t)P₃(t)








P₂(t)P₃(t)




_x( P₂ (x)P₃(x))

Рис. 14. Граф вывода заключения

2.2.4 Принцип резолюции

Если матрица формулы в результате приведения к виду ПНФ не будет содержать свободных переменных и сколемовских функций, то для вывода заключения полностью пpuменим алгоритм принципа резолюции, рассмотренный в исчислении высказываний. Этот алгоритм основывается на том, что если две формулы состоящие из дизъюнкции атомов (в дальнейшем такие формулы будем называть дизъюнктами ) связаны конъюнкцией, и в них имеются два одинаковых или приводимых к одинаковым (унифицируемых ) атома с разными знаками, то из них можно получить третий дизъюнкт , который будет логическим следствием первых двух, и в нем будут исключены эти два атома. Однако, если в результате приведения к виду ССФ аргументы атомов содержат сколемовские функции, то для поиска контрарных атомов необходимо выполнить подстановки термов вместо предметных переменных и получить новые формулы дизъюнктов, которые допускают их унификацию при формировании контрарных пар. Множество подстановок нужно формировать последовательно, просматривая каждый раз только одну предметную переменную.

---

Например, если даны два дизъюнкта (P₁(x)P₂(x)) и (P₁(f(x))P₃(y)), то для получения контрарной пары атомов возможна подстановка

_x^f(х)(P₁(x)P₂(x))=(P₁(f(x))P₂(f(x))) и

_x^f(х)(P₁(f(x))P₃(y))= (P₁(f(x))P₃(y)).

В результате склеивания этих дизъюнктов может быть получена резольвента: (P₁(f(x))P₂(f(x)))(P₁(f(x))P₃(y))= (P₂(f(x)) P₃(y)).

Если пара дизъюнктов имеет вид (P₁(f₁(x))P₂(x)) и (P₁(f₂(x))P₃(y)), то никакая подстановка не позволит сформировать резольвенту.
Пример: Даны две формулы P³(a;x;f(q(y))) и P³(z;f(z);f(u)).

Выполнить унификацию контрарных атомов.

1) _z^a P³(z;f(z);f(u))=P³(a;f(a);f(u));

2) _x^f(a) P3(a;x;f(q(y)))=P³(a;f(a);f(q(y)));

3) _u^q(y) P³(a;f(a);f(u))=P³(a;f(a);f(q(y))).

В результате получены два контрарных атома: P³(a;f(a);f(q(y))) и P³(a;f(a);f(q(y))). Если в эти формулы атомов вместо предметной переменной y сделать подстановку предметной постоянной b, т.е.

_y^bP³(a;f(a);f(q(y)))=P³(a;f(a);f(q(b))) и

_y^bP3(a;f(a);f(q(y)))= P³(a;f(a);f(q(b))),

то получим два контрарных высказывания.

Пример. Даны две формулы P³(x;a;f(q(a))) и P³(z;y;f(u)).

Выполнить унификацию контрарных формул.

1) _x^bP³(x;a;f(q(a)))=P³(b;a;f(q(a)));

2) _y^a P³(z;y;f(u))=P³(z;a;f(u));

3) _y^aP³(z;a;f(u))=P³(b;a;f(u));

_{4) u}^q(a)P³(b;a;f(u))=P³(b;a;f(q(a))).

В результате получены две контрарных формулы: P³(b;a;f(q(a))) и P³(b;a;f(q(a))).

Принцип резолюции может быть усилен линейным выводом, упорядочением атомов в дизъюнкте и использо­ванием информации о резольвируемых атомах.

Линейным выводом из множества дизъюнктов K называется последовательность дизъюнктов D₁, D₂,...D_n, где каждый член D_iK, а каждый D_i+1 является резольвентой центрального дизъюнкта (или предшествующей резольвенты) и бокового дизъюнкта из множества K.

Упорядоченным дизъюнктом называется дизъюнкт с заданной последовательностью атомов. Атом P_j

---