Решение задач дедуктивного выбора
В дедуктивных моделях представления и обработки знании решаемая проблема записывается в виде утверждении формальной системы, цель-в виде утверждения, справедливость которого следует установить или опровергнуть на основании аксиом (общих законов) и правил вывода формальной системы. В качестве формальной системы используют исчисление предикатов первого порядка.
В соответствии с правилами, установленными в формальной системе, заключительному утверждению-теореме, полученной из начальной системы утверждений (аксиом, посылок), приписывается значение ИСТИНА, если каждой посылке, аксиоме также приписано значение ИСТИНА.
Процедура вывода представляет собой процедуру , которая из заданной группы выражений выводит отличное от заданных выражение.
Обычно в логике предикатов используется формальный метод доказательства теорем, допускающий возможность его машинной реализации, но существует также возможность доказательства неаксиоматическим путем : прямым выводом, обратным выводом.
Метод резолюции используется в качестве полноценного (формального) метода доказательства теорем.
Для применения этого метода исходную группу заданных логических формул требуется преаобразовать в некоторую нормальную форму. Это преобразование проводится в несколько стадий, составляющих машину вывода.
