Алгоритм приведения к виду Хорна.

Клаузальная форма. Клаузы Хорна.

Еще пример. Доказать равносильность формул F и G.

Пример. Доказать равносильность формул F и G.

F=Ø("x)($y)[S(x)ÙP(x,y)Þ($z)(T(z)ÙP(x,z))]

G=($x)("y)[S(x)ÙP(x,y)Ù("z)(T(z)ÞØP(x,z))]

1. Исключение импликации

F=Ø("x)($y)[Ø(S(x)ÙP(x,y))Ú($z)(T(z)ÙP(x,z))]

2. F=($x)("y)[ØØ(S(x)ÙP(x,y))ÙØ($z)(T(z)ÙP(x,z))]

3. F=($x)("y)[ (S(x)ÙP(x,y))Ù("z)(ØT(z)ÚØP(x,z))]

4. F=($x)("y)[S(x)ÙP(x,y)Ù("z)(T(z)ÞØP(x,z))] = G

F=Ø("x)P(x)Þ[($x)("y)Ø(H(x,y)ÙS(x)) ÚØ($y)(Q(x,y)ÞP(y))]

G=("x)P(x)Ú[($x)("y)(H(x,y)ÞØS(x))Ú("y)[Q(x,y)ÙØP(y))]

1. HÞG=ØHÚG - исключение импликации

F=("x)P(x)Ú[ ($x)("y)Ø(H(x,y)ÙS(x)) ÚØ( $y)(ØQ(x,y)ÚP(y)) ]

2. Ø(HÚG)=ØHÙØG

F=("x)P(x)Ú[ ($x)("y)(ØH(x,y)ÚØS(x)) Ú ("y)(Q(x,y)ÙØP(y))]

3. F=("x)P(x)Ú[ ($x)("y)(ØØH(x,y)ÞØS(x)) Ú ("y)(Q(x,y)ÙØP(y))]

 

Формулы в идее Хорна имеют вид:

z ¬ P1,p2,…Pk

z и pi – предикаты или их отношения

z ¬P1ÙP2Ù … ÙPk

Если клаузы выглядят так ¬P1ÙP2Ù … ÙPk, то это заведомая ложь.

А если так: z ¬ , то это факт.

Пример. Пусть имеются предикаты:

M(x,y) = x mother of y

O(x,y) = x father of y

D(x,y) = x dad of y

Запишем правила Хорна.

D(x,y)¬O(x,z), M(z,y)

D(x,y)¬O(x,z), O(z,y)

Любую логическую формулу можно преобразовать к одному или нескольким правилам Хорна с помощью следующей последовательности действий.

1) Исключение знака импликации Þ и эквивалентности Û. (Законы 1 и 2)

2) Продвижение знака отрицания до атома (предиката) или атомарной формулы (законы 15, 16, 17, 29, 30)

3) Стандартизация переменных (переименование). Связанные переменные в случае, если они встречаются в других частях формул. переименовываются.

4) Вынесение кванторов, т.е. получение предваренной формы.

5) Избавление от кванторов существования по следующим правилам:

* Если левее удаляемого квантора существования нет ни одного квантора всеобщности, то квантор существования отбрасывается, а его переменная заменяется на символ константы, отличной от символов констант, уже имеющихся в формуле.

* Если левее удаляемого квантора существования есть n кванторов всеобщности, то квантор существования отбрасывается, а его переменная заменяется на n местный функциональный символ, отличный от функциональных символов уже имеющихся в формуле.

6) Кванторы всеобщности отбрасываются.

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

AÙ(BÚC)=(AÙB)Ú(AÚC)

AÙ(BÙC) = AÙBÙC

AÚ(BÚC)=AÚBÚC

A1ÚA2ÚA3Ú(B1ÙB2ÙB3) = (A1ÚA2ÚA3ÚB1)Ù(A1ÚA2ÚA3ÚB2)Ù(A1ÚA2ÚA3ÚB3)

8) Запись в виде множества дизъюнктивов S={D1,D2..Dn)

9) Каждый дизъюнкт записывается в виде одного правила Хорна:

ØAÚB=AÞB

ØAÚØBÚC=C¬AÙB