Получение дизъюнктов

Основные равносильности для предикатов

Для нас имеют смысл и значение только интерпретированные предикаты. То есть предикаты, которым поставлены в соответствия некоторые отношения (одномерным предикатам – свойства). В результате, предикаты дают некоторые содержательные высказывания относительно объектов рассматриваемых областей. Если соответствующее высказывание истинно, то говорят, что оно выполняется в данной интерпретации.

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

1. ¬"x P(x) º $x ¬P(x)

2.¬$x P(x) º "x ¬P(x)

3. ¬"x ¬P(x) º $x P(x)

4. ¬$x ¬P(x) º "x P(x)

5. "x P(x) Ú Q ) (предикат Q не зависит от x.)

6. "x P(x) & Q º "x ( P(x) & Q )

7. $x P(x) Ú Q º $x ( P(x) Ú Q )

8. $x P(x) & Q º $x ( P(x) & Q )

9. "x Q º Q

10. $x Q º Q

11. "xP(x) & "xR(x) º "x ( P(x) & R(x) )

12. $xP(x) Ú $xR(x) º $x ( P(x) Ú R(x) )

13. "xP(x) Ú "xR(x) ® "x ( P(x) Ú R(x) )

14. $x (P(x) & R(x) ) ® $xP(x) & $xR(x)

15. "x P(x) º "yP(y) (х, у - из одной предметной области)

16. $x P(x) º $y P(y)

17. "x$y P(x, y) º $x"y P(x, y)

18. "x"y P(x, y) º "x"y P(x, y)

19. $x$y P(x, y) º $x$y P(x, y)

Важное замечание. Рассматриваем только замкнутые предикаты,то естьпредикаты, не содержащиесвободных вхождений переменных.

В общем случае необходимо пройти три этапа:

1. Получить предваренную нормальную форму.

2. Произвести сколемизацию.

3. Получить дизъюнкты.

Предваренная нормальная форма - такая форма представления предиката, когда все кванторы вынесены в начало за скобки (кванторная приставка), а в скобках есть только операции дизъюнкции, конъюнкции и отрицания. При этом символы отрицания, если таковые имеются, стоят непосредственно перед символами предикатов.

Сколемизация(от фамилии математика - Skölem)позволяет получать запись замкнутого предиката в форме без кванторов.

Избавляемся от кванторов существования:

1) Если левее нет кванторов общности, то

соответствующая переменная заменяется константой сколема;

2) Иначе переменная заменяется функцией сколема от переменных, на которые навешаны кванторы общности, стоящие левее данного квантора существования.

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

Пример:

¬"x ( "yP(x, y) Ú ¬$zR(z) ® Q(x) & "yM(x, y)) º

º ¬"x ( $y¬P(x, y) & $zR(z) Ú Q(x) & "yM(x, y) ) º

º $x ( ("yP(x, y) Ú "z¬R(z)) & (¬Q(x) Ú $y¬M(x, y)) ) º

º $x ( "yz (P(x, y) Ú ¬R(z)) & $y( ¬Q(x) Ú ¬M(x, y)) ) º

º $x"y"z$h ( (P(x, y) Ú ¬R(z)) & ( ¬Q(x) Ú ¬M(x, h)) ) º

º (P(a^c, y) Ú ¬R(z)) & (¬Q(a^c) Ú ¬M(a^c, f^c(y, z)))

Каждая элементарная дизъюнкция в полученном выражении является дизъюнктом.