Логическое программирование на языке Visual Prolog. Солдатова О.П - 12 стр.

UptoLike

ВУЗ: 

СГАУ | Самара

Составители: 

Рубрика: 

12
Для любых двух дизъюнктов C
1
и C
2
, если существует литерал L
1
в C
1
,
который контрарен литералу L
2
в C
2
, то вычеркнув L
1
и L
2
из C
1
и C
2
соответственно и построив дизъюнкцию оставшихся дизъюнктов, получим
резолюцию (резольвенту) C
1
и C
2
.
Пример 4: рассмотрим следующие дизъюнкты:
C
1
: P
∨
R,
C
2
:
¬
P
∨
Q.
Дизъюнкт C
1
имеет литерал P, который контрарен литералу
¬
P в C
2
.
Следовательно, вычеркивая P и
¬
P из C
1
и C
2
соответственно, построим
дизъюнкцию оставшихся дизъюнктов R и Q и получим резольвенту R
∨
Q.
Важным свойством резольвенты является то, что любая резольвента
двух дизъюнктов C
1
и C
2
есть логическое следствие C
1
и C
2
. Это
устанавливается в следующей теореме.
Теорема 4. Пусть даны два дизъюнкта C
1
и C
2
. Тогда резольвента C
дизъюнктов C
1
и C
2
есть логическое следствие C
1
и C
2
.
Если есть два единичных дизъюнкта, то их резольвента, если она
существует, есть пустой дизъюнкт . Более существенно, что для
невыполнимого множества дизъюнктов многократным применением правила
резолюций можно породить .
Определение 5: Пусть S – множество дизъюнктов. Резолютивный
вывод C из S есть такая конечная последовательность С
1
, C
2
,…, C
k
дизъюнктов, что каждый C
i
или принадлежит S или является резольвентой
дизъюнктов, предшествующих C
i
, и C
k
=C. Вывод из S называется
опровержением (или доказательством невыполнимости ) S.
Пример 5. Рассмотрим множество S:
1.
¬
P
∨
Q,
2.
¬
Q,
3. P.
Из 1 и 2 получим резольвенту
4.
¬
P.
Из 4 и 3 получим резольвенту
5. .
Так как
получается из S применениями правила резолюций, то
согласно теореме 4
есть логическое следствие S, следовательно, S
невыполнимо.
Метод резолюций является наиболее эффективным в случае
применения его к множеству Хорновских дизъюнктов.
Определение 6: Фразой называется дизъюнкт, у которого негативные
литералы размещаются после позитивных литералов в конце дизъюнкта.
Пример 6: Р
1
∨
Р
2
∨
…Р
n
∨
¬
N
1
∨
¬
N
2
…
∨
¬
N
m
Определение 28: Фраза Хорна это фраза, содержащая только один
позитивный литерал.
Пример 7: преобразовать фразу Хорна в обратную импликацию.

Страницы