машина вывода

Машина вывода — программа, которая выполняет логический вывод из предварительно построенной базы фактов и правил в соответствии с законами формальной логики. * Факт в данном случае — утверждение, являющееся постоянно истинным, например: «Адам является человеком». * Правило в данном случае — параметризованное утверждение, состоящее из двух частей: условия и результата, например: «Если X является потомком человека, то X является человеком». В данном примере правило определяет условие «X является потомком человека». Если для значения параметра X это условие истинно, то правило превращается в факт «X является человеком». Для построения базы фактов и правил применяются формальные языки, обычно напоминающие естественный язык, но гораздо более строгие и ограниченные. Машина вывода обычно может выполнять одну или обе из следующих операций: * Проверка истинности некоторого факта — истинным считается факт, если он может быть выведен по законам формальной логики из имеющейся базы фактов и правил. * Нахождение множества значений параметра некоторого правила, при котором данное правило превращается в истинный факт. В первом случае на вопрос типа «Истинно ли A?» машина вывода даёт ответ «Да» либо «Нет», во втором — на вопрос типа «При каких X истинно правило A(X)?» машина вычисляет все возможные значения X, при подстановке которых в правило A это правило превращается в истинный факт. В теории построения машин логического вывода не имеет однозначного решения так называемая — проблема способа определения не-истинности факта. В большинстве случаев машина вывода делает вывод о не-истинности факта, если истинность факта не является выводимой из базы фактов и правил, но это может приводить к неправильной интерпретации знаний, поскольку результаты «A ложно» и «A недоказуемо» не различаются. Машина вывода является базовым элементом экспертных систем и систем исполнения программ, написанных на языках логического программирования, таких как Prolog.