Алгоритм перевода в СКНФ. Метод резолюции и правило факторизации

Пусть имеются формулы A1,..Am и B. Требуется доказать, что  из

формул A1,..Am можно вывести B. Т.к. ØA1Ú…ÚØAmÚB(следствие из теоремы о полноте). Обр-я теорема: A1Ù…ÙAmÙØB. Для этого сначала

приводят к сколемовской конъюнктивной нормальной форме:

1)ограничение свободных перем-х. Если х1,..xn – свободные перем-е,

содержащ. в А, то преобразуется к виду $x1.. $x, A.

2)переимен. перем-х, чтобы различн. перем-е имели разные имена.

3)удаление символа É. AÉB заменить формулой ØAÚB.

4)перемещение символа Ø внутрь формул с символами Ù,Ú,",$ пока Ø

не станет относится к атомам. Для этого используем правило:

Ø(AÙB)-> ØAÚØB

Ø(AÚB)-> ØAÙØB

Ø ØA->A

Ø " xA-> $xØ A

Ø $ xA-> "xØ A

5)удаление символа $. Все переем-е, связанные с квантором $, замен.

сколемовскими константами или функ-ми. Если переем-я введена вне

области действия квантора ", то она заменяется константой. В против-

ном случае переем-я заменяется функ-ей от значений введенных квантором " перем-х, в области дей-я которых она была введена.

 $x"y"z$u P(x,y,z,u) -> "y"z P(a,y,zf(y,z))

6)перемещение символов " вперед и отбрасывание ". Все свободные

перем-е считаются введенными квантором ".

7)перемещение символа Ú относительно Ù. Используя правило

(АÙВ)ÚС -> (AÚC)Ù(BÚC)

8)hhhhразделение формул на набор дизъюнктов(предложений).

9)минимизация. Атом с Ø или без Ø называется литералом. Удаля-

ются повторяющиеся литералы. Удаляются предложения, литералы которых  взаимно отрицают друг друга.

A1Ú…ÚAmÚØB1Ú…ÚØBm представ. в форме клаузы A1…Am->B1…Bm.

Предложение с m=1 и n=0 соответствует факту в Прологе.

Предложение с m=1 и n>=1 соответствует правилу в Прологе.

Предложение с m=0 и n>=1 соответствует запросу в Прологе.

Метод резолюций: 

Пусть есть 2 предлож-я C1=A1Ú…ÚAmÚD и С2=B1Ú…ÚBnÚØD. Резольвентой этих предл-ий явл-ся C=A1Ú…ÚAmÚB1Ú…ÚBn. Если литералы D и ØD не равны, но существует унификатор, делающий их

равными, то наиболее общий унификатор для D и ØD применяется к предложениям C1 и C2, а затем вычисляется резольвента. Если резол.

С пуста, то это указывает на невыполниость исходной формулы.

В случае нехорновских дизъюнктов метод резолюции необходимо дополнить правилом факторизации, которое удаляет повторяющиеся

литералы в одном предложении. Если литералы не равны, то также выполняется их унификация.