Фразы Хорна ( Horn clause )

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)      выполняется