Главная arrow Логика arrow Простой логический вывод
Как начинался компьютер
Компьютерная революция
Двоичный код
Разработки военных лет
Интегральные микросхемы
Микрокомпьютер
Персоны
Сеть
Язык компьютера
Развитие ПО
Гибкие системы
Средства разработки
Информатика
Вычислительная наука
Операционные системы
Искусственный интеллект
Предыстория
Поиск
Знания и рассуждения
Логика
Робототехника
 

 
Простой логический вывод Печать

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

Следует отметить, что факт не является "новым", если он представляет собой переименование известного факта. Одно высказывание называется переименованием другого, если оба эти высказывания идентичны во всем, за исключением имен переменных. Например, высказывания Likes (х, IceCream) и Likes (у, IceCream) представляют собой переименования по отношению друг к другу, поскольку они отличаются лишь выбором имени переменной, х или у; они имеют одинаковый смысл — все любят мороженое.

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

 

function FOL-FC-Ask(.KB, a) returns подстановка или значение false

  inputs: KB, база знаний - множество определенных выражений

    первого порядка

    а, запрос - атомарное высказывание

  local variables: new, новые высказывания, выводимые

    в каждой итерации

  repeat until множество new не пусто

  new <— {}

  for each высказывание г in KB do

  (Pi л ... л Pn => q) <r- Standardize-Apart (r)

  for each подстановка 6, такая что Subst F,р1Л...лрь) =

  Subst {QfPi* л...лрп1) для некоторых р±' ,...,Рп'

  в базе знаний KB

  д' <- Subst @, д)

  if выражение д' не является переименованием

    некоторого высказывания, которое уже находится

    в KB, или рассматривается как элемент множества

  new then do

  добавить д' к множеству new

  ф <- Unify(g', а)

  if значение ф не представляет собой fail

  then return ф

    добавить множество new к базе знаний KB

return false

 

Для иллюстрации работы алгоритма FOL-FC-Ask воспользуемся описанной выше задачей доказательства преступления. Импликационными высказываниями являются высказывания, приведенные в уравнениях 9.3, 9.6-9.8. Требуются следующие две итерации.

  • В первой итерации правило 9.3 имеет невыполненные предпосылки. Правило 9.6 выполняется с подстановкой {х/М^ и добавляется высказывание Sells (West, Mlt Nono). Правило 9.7 выполняется с подстановкой {х/М^ и добавляется высказывание Weapon (Mi). Правило 9.8 выполняется с подстановкой {x/Nono} и добавляется высказывание Hostile{Nono).
  • На второй итерации правило 9.3 выполняется с подстановкой {x/West, y/Mlf z/Nono} и добавляется высказывание Criminal (West).

Сформированное дерево доказательства показано на рисунке. Обратите внимание на то, что в этот момент невозможны какие-либо новые логические выводы, поскольку каждое высказывание, заключение которого можно было бы найти с помощью прямого логического вывода, уже явно содержится в базе знаний КВ. Такое состояние базы знаний называется фиксированной точкой (fixed point) в процессе логического вывода. Фиксированные точки, достигаемые при прямом логическом выводе с использованием определенных выражений первого порядка, аналогичны фиксированным точкам, возникающим при пропозициональном прямом логическом выводе; основное различие состоит в том, что фиксированная точка первого порядка может включать атомарные высказывания с квантором всеобщности.


Дерево доказательства, сформированное путем прямого логического вывода в примере доказательства преступления. Первоначальные факты показаны на нижнем уровне, факты, выведенные логическим путем в первой итерации, — на среднем уровне, а факт, логически выведенный во второй итерации, — на верхнем уровне.

Свойства алгоритма FOL-FC-Ask проанализировать несложно. Во-первых, он является непротиворечивым, поскольку каждый этап логического вывода представляет собой применение обобщенного правила отделения, которое само является непротиворечивым. Во-вторых, он является полным применительно к базам знаний с определенными выражениями; это означает, что он позволяет ответить на любой запрос, ответы на который следуют из базы знаний с определенными выражениями.

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

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

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

NatNum(0)

Vn NatNum(n) => NatNum(S{n))

то в результате прямого логического вывода будут добавлены факты NatNum (S0)), NatNum(S(S{0) ) ), NatNum(S(S(S0) ) ) ) и т.д. Вообще говоря, избежать возникновения этой проблемы невозможно. Как и в общем случае логики первого порядка, задача определения того, следуют ли высказывания из базы знаний, сформированной с использованием определенных выражений, является полуразрешимой.