Прямая система дедукции

Рассмотрим следующий способ построения машины доказательства — ядра интеллектуальной системы логического вывода в форме системы дедукции на основе правил. Так же, как эго принято в логическом программировании, мы должны разделить все множество формул, всю информацию, которая у нас есть в данной предметной области на три класса — факты, правила и цели. При этом накладываются следующие синтаксические ограничения:

• • то, что мы будем считать фактами, на самом деле ничем не ограничено и может быть представлено в любой форме И/ИЛИ;
• • то, что мы будем считать правилами, обязательно должно иметь вид L —" W, где L — литерал, a W — любая формула, которая будет представлена в форме И/ИЛИ;
• • цель должна быть дизъюнкцией литералов, т. е. дизъюнктом. Другими словами, можно сформулировать условие остановки: целевая формула является дизъюнктом, граф решения заканчивается в целевых литералах.

Смысл процедуры наращивания графа И/ИЛИ с помощью правил прост. Возьмем факт (или множество фактов) и представим их в форме И/ ИЛИ. Получится гиперграф. Начнем к листовым узлам этого графа прицеплять правила. Каждый листовой узел построенного графа унифицируется с левой частью правила. Если унификация успешна, мы наращиваем граф (или дерево) И/ИЛИ правой частью правила, пока в этом графе не появится граф решения, листья которого попадают в целевые узлы (т.е. унифицируются с целевыми литералами). Когда происходит отождествление левой части правила с листовым узлом в графе, возможно, потребуется выполнение некоторых подстановок для унификации. Понятно, что если в разных графах решения применяются разные правила, то они применяются независимо. Но в одном графе решения невозможно одновременно подставить вместо одной и той же переменной разные термы. Значит, такие случаи должны быть исключены. Фактически, механизм, который сейчас описывается, является частным случаем метода резолюций, который проводится с помощью перестроения графа.

Пример 4.9.

Факт: Власенко умный и знает метод резолюций или он не студент.

— iC (B)v (P (B)_Ay (B".

Правило 1: Все учащиеся группы 5057 являются студентами -iC (x) —> -i5057®.

Правило 2: Тот, кто знает метод резолюций, является отличником Р (У) -> О (у).

Цель: Существует некто, кто или не учится в группе 5057 или является отличником 32 -i5057(z) v O (z).

На примере правила 1 видно преимущество прямой системы на основе правил. Эксперт предметной области — «инженер знаний» — конструируя систему представления знаний, имеет возможность правило — «все учащиеся группы 5057 являются студентами» — сразу записать в контрапозитивном виде: «если он не студент, то он не учится в группе 5057». Тем самым конструктор системы представления знаний (человек) дает подсказку программе логического вывода: в дедуктивных системах рассуждать выгоднее от общего к частному, а не от частного к общему. Именно это и сделано в правиле 1. Вот почему сохранение импликативности так важно и полезно.

Мы строим прямое дедуктивное рассуждение, а не метод резолюций, поэтому отрицание к цели применять не следует. Цель должна использоваться в том виде, в котором находится в формулировке задачи. В данном случае видно, что после сколемизации цель будет бескванторной дизъюнкцией литералов, что и требуется в синтаксическом условии прямой системы дедукции.

Ход рассуждения таков (рис. 4.2).

В начальный момент граф фактов имеет следующий список листовых узлов: —"С (В), Р (В) и У (В). Используем наше правило 1 для наращивания дерева. Левая часть правила унифицируется с подстановкой [В/дг]. Дерево наращивается правой частью, которая унифицируется с первым целевым литералом. Эго еще не решение, поскольку мы не построили граф решения, который заканчивается целевыми литералами. Поэтому продолжаем применять правила. Срабатывает правило 2, и результат отождествляется со вторым целевым литералом.

Рис. 4.2. Расширение формы И/ИЛИ применением правил.

Построен граф решения, который заканчивается целевыми литералами (па рис. 4.2 обведен). Чтобы сохранить информацию о подстановках, мы вводим дуги соответствия (на рисунке они изображены толстыми незакрашенными стрелками), соединяющие заменяемые литералы и левые части правил.

Рассмотрим еще один пример.

Пример 4.10.

Дан факт: P (x)vQ (x).

Правило 1: Р (Л) -> R (A).

Правило 2: Q (B) —> R (B), где А и В — конкретные константы.

Цель: R (A)vR (B).

Заметим, что цель не является логическим следствием фактов. Этот пример объясняет, в чем значения ограничения, говорящего о том, что подстановки на дугах соответствия в одном графе решения должны быть согласованы (рис. 4.3).

Рис. 43. Несогласованные подстановки на дугах соответствия.

Видно, что подстановки не совместимы: нужно одновременно подставить Л вместо х и В вместо х. В результате подстановки не согласованы, граф решения нс построен, как и должно быть, потому что цель не является логическим следствием фактов и правил.

Мы провели в технике графов резолютивный вывод, но применимость этого приема ограничена тем, что у нас есть синтаксические ограничения на вид фактов, синтаксические ограничения на вид правил и синтаксические ограничения на вид целей.