yandex rtb 1
ГоловнаЗворотній зв'язок
yande share
Главная->Математика і інформатика->Содержание->5.5. Метод резолюций для логики высказываний.

Математическая логика

5.5. Метод резолюций для логики высказываний.

Основная идея метода резолюций состоит в том, чтобы проверить, содержит ли множество S пустой дизъюнкт О. Если S содержит , "то множество S невыполнимо, если нет, то надо проверить, может ли он быть получен из данного множества дизъюнктов. Иными словами, необходимо найти множество основных примеров, опровергающих исходное множество дизъюнктов. Эта процедура основана, на правиле резолюции.

Правило резолюции Робинсона. Для любых двух дизъюнктов С1 и С2 если существует литера L1C1 и контрарная ей литера L2С2 (L2=¬L1), то вычеркнув L1 из С1 и L2 из С2 и построив дизъюнкт из оставшихся литер, получим резольвенту С1 и C2 : C`1vC'2.

Теорема 6.5. Резольвента С есть логическое следование С1 и С2, содержащих контрарные литеры L и ¬L.

Определение 5.12. Резолютивный выводу из множества дизъюнктов S есть последовательность C1, C2, … ,Ck, такая что каждое С, либо принадлежат S, либо является резольвентой предшествующих Q и, если последний дизъюнкт Ck= , то множество дизъюнктов S является невыполнимым, а весь вывод называется опровержением S. Если Ск не является пустым дизъюнктом и дальнейшее применение правила резолюции невозможно, то множество S является выполнимым.

Пример.    Рассмотрим    задачу    из    главы    2.    Необходимо    проверить логическое, следование: PS, SR,|P |= R. Составим множество S,  для  чего  каждую  формулу приведем  к  КНФ,  а  от  возьмём отрицание. Получим:

1.   PvS

2.   SvR

3.    Р

4.    R

5.    S           резольвента 4,2

6.    Р           резольвента 5,1

7.              резольвента 3,6

5.5, Метод резолюций для логики первого порядка.

Применение метода резолюций в логике первого порядка усложняется тем, что дизъюнкты содержат переменные, которые могут не совпадать в двух одинаковых литерах. Например, C1 = P(x)vQ(x), C2=P(f(x))vV(x). В этих дизъюнктах нет контрарных литер, однако, если мы подставим f(a) вместо х в С1 и а вместо х в С2, то получим Cl=P(f(a))vQ(f(a)), C2=P(f(a))vV(a), где литеры P(f(a)) и P(f(u)) будут уже контрарны. Получим резольвенту Q(f(a))vV(a). Подстановка {а/x } в С2 и {f(a)/x } в С1 насыпается унификацией, а множество {а/х, Г(а)/х} называется унификатором.

В общем случае, подставив f(x) вместо х в С1, получим резольвенту Q(f(x))vV(x). Подстановка (f(x)/x), которая выполняется для обоих дизъюнктов, называемся наиболее общим унификатором.

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

Определение 5.13. Если две или более литер (с одинаковым знаком) дизъюнкта С имеют наиболее общин унификатор , то С называется склейкой С. Если С - единичный дизъюнкт, то склейка называется единичной склейкой.

Пример. Пусть C=P(x)vP(f(v))v ¬Q(x). Тогда  первая  и  вторая литеры -(подчеркнутые)      имеют      наиболее      общий      унификатор      ={f(у)/х}. Следовательно, C=P(f(y))v¬Q(f(y)) есть склейка С.

Определение 5.14. Пусть С1 и С2 - два дизъюнкта (называемые дизъюнктами-посылками), которые не имеют никаких общих переменных. Пусть L1 и L2 - две литеры в С1 и С2 соответственно. Если L1 и ¬L2 имеют наиболее общий унификатор , то дизъюнкт (C1-L1 )v(C2 -L2) называется (бинарной) резольвентой С1 и С2. Литеры L1 и L2 называются отрезаемыми литерами.

Определение 5.15. Резольвентой дизъюнктов-посылок С1 и С2 является одна из следующих резольвент:

1) бинарная резольвента С1 и С2

2) бинарная резольвента С1 и склейки С2

3) бинарная резольвента С2 и склейки С1

4) бинарная резольвента склейки C1 и склейки С2.

Пример. Пусть C1=P(x)vP(f(y))vR(g(y)) и C2=¬Fl(f(g(a)))vQ(b). Склейка С1 есть С1'=P(f(y))vR(g(y)). Бинарная резольвента С1 и С2 есть R(g(g(a)))vQ(b). Следовательно, R(g(g(a)))vQ(b) есть резольвента С1 и С2.

 

35