|
Читайте также: |
Правила резолюции – берутся 2 выражения, и выражаются новые выражения, содержащие все литералы 2х первоначальных выражений, за исключение 2х взаимообратных литералов.
Есть множество фраз:
Нужно выяснить является ли фраза P(a) следствием существующего множества фраз. На 1 шаге добавим к остальным фразам отрицание P(a). В результате получим:
Алгоритм реализуется с помощью 2х правил:
1. в 1ой выполненной резолюции следует использовать только что добавленное отрицание фразы.
2. в каждой последней резолюции должна участвовать резольета предыдущей резолюции.
В соответствии с 1 правилом в 1ой резолюции принимает участие фраза (10) и она резольируется с фразой (6). в результате чего получается 
Согласно правилу 2 в следующей резолюции должна учитываться фраза (11) и она резольируется с фразой (7). Результатом будет фраза 
Все переменные из исходной для R-формулы заменены во фразе (12) на константы. Фраза (12) резольируется с фразой (9), что приводит к образованию пустой фразы => обнаружено противоречие. В виду того, что добавление 
P(a) к существующему множеству фраз приводит к противоречию, P(a) является следствием множества фраз.
Дата добавления: 2015-07-10; просмотров: 103 | Нарушение авторских прав