![]() |
![]() |
p ← q1,..., qn, где p – один литерал, q1,...,qn – последовательность утверждений.
В ПРОЛОГе: p :- q1,...,qn
Рассмотрим пример, как на основании использовании метода опровержения строится дерево вывода. Пусть нам необходимо определить возможность покупки клиентом компьютера. Он будет на нем играть, и ему необходимо, чтобы в нем был графический ускоритель GeForce2.
Купит (клиент, компьютер):-Любит (клиент, комп. игры)
Имеет (компьютер, граф. ускоритель)
Дерево доказательства строится сверху вниз. Каждая ветвь связывает две родительские фразы, в которых содержатся дополняющие литералы, с фразой, которая образуется в результате применения правила резолюции. Ко всем целям, записанным справа от знака «следует» (:-), неявно применяется отрицание (или принцип обратного дерева). В левой части дерева представлены формулы целей, а в правой – фразы из базы данных.
Цель: Купит(Клиент1, Компьютер1).
Пусть в базе данных содержится два истинных утвеждения:
Любит (Клиент1, Action )
Имеет (Компьютер1, GeForce 2)
Метод резолюции (обратного вывода) заключается в следующем: в базе данных вводится правило, которое содержит отрицание цели, и оно проверяется, пока не будет найдено противоречие (т.е. правило верно) или оно будет подтверждено.
Goal :- Купит(Клиент1, Компьютер1)
Купит (клиент, компьютер):-Любит (клиент, комп. игры)
Имеет (компьютер, граф. ускоритель)
:-Любит (Клиент1, комп. игры), Имеет (Компьютер1, граф. ускоритель)
Любит (Клиент1, Action ) выполняется
Имеет (Компьютер1, GeForce 2) выполняется
![]() |
![]() |