Составители:
Рубрика:
4
ние порождается некоторым предикатом, а каждый предикат соответ-
ствует множеству высказываний.
Задача ПРОЛОГ – программы заключается в том, чтобы доказать,
является ли заданное целевое утверждение следствием из имеющихся
фактов и правил.
Решаемая задача представляется в виде совокупности утверждений
(аксиом), цель задачи также записывается в виде утверждения. Тогда
решение задачи представляет собой выяснение логического следования
из аксиом
(А
1
∧ А
2
∧ А
3
∧ ... А
n
)→ В.
На практике удобно использовать доказательство от противного, т. е.
доказывать невыполнимость. Если A → B истинно, то
AB
→
ложно и
A ∨
B
ложно.
На этом основан принцип резолюции, который требует представле-
ния формул исчисления предикатов в виде набора дизъюнктов, связан-
ных операцией конъюнкции [конъюнктивная нормальная форма (КНФ)].
Правило резолюции имеет вид
(X ∨ A) ∧ (
A
∨ Y) → (X ∨ Y).
Правило резолюции позволяет соединить две формулы, из одной уда-
лив А, а из другой
A
. В этом случае говорят, что A и
A
резольвируют.
Главная идея метода резолюции заключается в проверке того, содер-
жит ли множество дизъюнктов R пустой (ложный) дизъюнкт. При по-
ложительном ответе формула, соответствующая R, невыполнима и со-
ответствующее утверждение противоречиво. Таким образом, доказав
невыполнимость формулы
(А
1
∧ А
2
∧ А
3
∧ ... А
n
) →
B
,
можно сделать вывод, что В истинно.
Рассмотрим пример использования метода резолюции, применяя до-
казательство от противного.
Пусть необходимо доказать истинность выражения
((P∨Q)∧(P→R)∧(Q→S))→(R∧S).
Для использования метода резолюции нужно рассмотреть конъюнк-
цию совокупности посылок и отрицания заключения в конъюктивной
нормальной форме. Для этого выполняется ряд шагов:
Страницы
- « первая
- ‹ предыдущая
- …
- 4
- 5
- 6
- 7
- 8
- …
- следующая ›
- последняя »
