8.1. Общие положения.

В дедуктивных моделях представления и обработки знаний решаемая проблема записывается в виде утверждений формальной логики. Цель – в виде утверждения, справедливость которого следует установить или опровергнуть на основании аксиом (общих законов) и правил вывода формальной системы. В качестве формальной системы обычно используется исчисление предикатов 1-го порядка [4;5].

В соответствии с правилами, установленными в формальной системе, заключительному утверждению – теореме, полученной из начальной системы утверждений (аксиом, посылок), приписывается значение 1 (истина), если каждой посылке и аксиоме также приписано значение 1. Формула В является логическим следствием формул тогда и только тогда, когда для любой интерпретации, в которой конъюнкция истинна, формула В также истинна.

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

В формальной логике установлено [4;5], что не существует эффективной разрешающей процедуры (алгоритма) для исчисления предикатов 1-го порядка, позволяющей выяснить по заданной формуле, является ли она теоремой или нет. Однако это ограничение, следуя тезису Гильберта (п.5.2), в большинстве случаев преодолевается в рамках усиленных вариантов формальной логики 1-го порядка [6;7].

8.2. Правило вывода по принципу резолюций.

В методе резолюции [5] исходная логическая формула приводится к специальному виду, называемому пренексной нормальной формой (ПНФ), имеющей вид:, где {}, , - предикатные переменные, М – бескванторная формула представленная в виде конъюнктивной нормальной формы (КНФ). С помощью функций Т. Сколема в данной ПНФ, сохраняя ее общезначимость, можно устранить кванторы существования и в итоге получаем стандартную форму.

Пример. Логическую формулу привести к стандартной форме.

Преобразуем данную формулу в ПНФ:

==

==

=.

Для устранения квантора введем функцию Сколема z=f(x;y). В результате получаем искомую стандартную форму в виде:

.

Обычно в стандартной форме ПНФ кванторы общности опускают, предполагая, что все переменные ими связанные являются универсально квантифицированными. Поэтому любая формула может быть представлена множеством дизъюнктов. В частности, в разобранном примере множество дизъюнктов S = {}, где запятая между дизъюнктами заменяет знак .

Из разобранного примера следует, что в методе резолюций общезначимость логической формулы устанавливается путем анализа множества дизъюнктов S: если оно не содержит ложных дизъюнктов, то ответ положительный; в противном случае данная формула общезначимой не является.

8.3. Дедуктивный вывод на семантических сетях.

Семантическая сеть, как отмечалось (п.6.2.1), представляет собой информационную модель предметной области знаний, которая включает факты и общие закономерности (аксиомы, посылки). В рамках логико-лингвистической модели [6] с каждой семантической сетью сопоставлена совокупность дизъюнктов вида: (что равно-сильно:), где – условия (), – заключения (). В семантической сети имеются два вида вершин – предикатные и дизъюнктные (коммутаторы) так, что предикатные вершины связаны между собой дугами только через коммутаторы [8],

Задача дедуктивного вывода в этом случае формулируется следующим образом. Дана логико-лингвистическая модель в виде семантической сети, с которой сопоставлен набор дизъюнктов указанного типа, и на ее вход подается ситуация, представленная совокупностью фактов . Эта ситуация, накладываемая на семантическую сеть, представляет собой текущее состояние системы обработки знаний, отражающее динамику ее изменения. Кроме того, на вход модели подается запрос, также приведенный к виду дизъюнктов.

Решение задачи дедукции состоит в получении противоречий в семантической сети по аналогии с установлением противоречия в принципе резолюции (п.8.2). Отметим, что в логико-лингвистической модели [6;7] процедура дедуктивного вывода основана на использовании многосортной логики предикатов 1-го порядка, что позволяет существенно ограничить область поиска необходимых утверждений, хотя сортность переменных может быть исключена введением соответствующих одноместных предикатов.

Среди алгоритмов уменьшения перебора при поиске нужной информации, а также быстрого и эффективного извлечения информации особо рассмотрим алгоритм, связанный с ракраской вершин данной семантической сети [7]. Правило раскраски следующее: в дизъюнкте ВА условие В будет раскрашено цветом 1, а заключение А – цветом 2, причем, поскольку вершины В и А соединены дугой через коммутатор g, то дуга до него изображается сплошной линией, а после него – пунктирной.

Пример. Для дизъюнкта имеем дизъюнктную вершину g (коммутатор), четыре предикатные вершины и четыре дуги: две непрерывные, идущие от вершины g к , и две пунктирные, идущие от g к .

Алгоритм дедукции на раскрашенных семантических сетях состоит в следующем [7]. Для предикатной вершины В подбирается любая контрарная пара (g;A), резольвирующая дизъюнкт g: ВА. Если исходная вершина В имеет другие контрарные пары, то они рассматриваются как альтернативные, но их выбор происходит только после неудачи с унификацией текущей контрарной пары (g;A). Если в вершину входят дуги только одного цвета, то они удаляются из рассмотрения, поскольку не влияют на вывод пустой сети (т.е. противоречия). Процесс продолжается до тех пор, пока не будет выявлена пустая сеть. Данный алгоритм позволяет обрабатывать сети большой размерности, однако он эффективен и полон только в таких системах обработки знаний, которые описываются набором хорновских дизъюнктов.

Лекция 9. Нечеткий вывод на знаниях.