Логический вывод

Напомним, что цель логического вывода состоит в том, чтобы определить, является ли истинным выражение KB \= а для некоторого высказывания а. Например, следует ли из базы знаний высказывание Р2,2? Рассматриваемый в данном разделе первый алгоритм логического вывода представляет собой непосредственную реализацию на практике определения логического следствия: перебрать (перечислить) все модели и проверить, является ли высказывание а истинным в каждой модели, в которой база знаний KB является истинной. Для пропозициональной логики модели представляют собой варианты присваивания значений true или false каждому пропозициональному символу. Возвратившись к примеру с миром вампуса, определим, что соответствующими пропозициональными символами являются B1,1, B2,1, P1,1, P1,2, P2,1, P2,2 и P3,1.

При наличии семи символов могут существовать 27=128 возможных моделей; в трех из них база знаний KB является истинной. В этих трех моделях является также истинным высказывание ¬P1,2 поэтому в квадрате [1,2] нет ямы. С другой стороны, высказывание P2,2 истинно в двух из трех моделей и ложно в одной из них, поэтому мы еще не можем определить, имеется ли яма в квадрате [2,2].

Истинностная таблица, которая сформирована для базы знаний, определенной в тексте главы. База знаний KB является истинной, если истинны высказывания R1-R5, а это происходит только в 3 из 128 строк. Во всех 3 строках высказывание P1,2 ложно, поэтому в квадрате [1,2] нет ямы. С другой стороны, яма в квадрате [2,2 ] может быть (или не быть)

 

Истинностная таблица

 

 

 

 

 

 

 

 

В таблице воспроизведен в более точной форме процесс формирования рассуждений, который проиллюстрирован на рисунке. Общий алгоритм определения логического следствия в пропозициональной логике приведен в листинге. Как и в алгоритме Backtracking-Search, приведенном на с. 131, функция TT-Entails? осуществляет рекурсивный перебор конечного пространства вариантов присваивания значений переменным. Этот алгоритм является непротиворечивым, поскольку он непосредственно реализует определение логического следствия, и полным, поскольку может применяться для любой базы знаний KB и любого высказывания а и всегда заканчивает свою работу, при условии, что количество моделей, подлежащих проверке, является конечным.

Алгоритм перебора истинностной таблицы для получения пропозициональных логических следствий, TT обозначает истинностную таблицу, функция PL-True? возвращает истинное значение, если некоторое высказывание является истинным в рамках некоторой модели. Переменная model представляет частично заданную модель — присваивание только некоторым переменным. Вызов функции Extend(Р, true,model) возвращает новую частично заданную модель, в которой высказывание Р имеет значение true

 

function TT-Entails?(KB, a) returns значение true или false

  inputs: KB, база знаний - высказывание в пропозициональной логике

  а, запрос - высказывание в пропозициональной логике

  symbols <— список пропозициональных символов в КБ и a

  return TT-Check-All(KB, a, symbols, [])

function TT-Check-All(KB, a, symbols, model) returns значение

  true или false

  if Empty?(symbols) then

  if PL-True?(KB, model) then return PL-True?(a, model)

  else return true

  else do

  P <— First(symbols); rest <— Rest(symbols)

return TT-Check-All(KB, a, rest, Extend(P, true, model) and

TT-Check-All(KB, a, rest, Extend(P, false, model)

 

Безусловно, выражение "является конечным" не всегда означает то же, что и выражение "является небольшим". Если КБ и а содержат в целом n символов, то количество моделей равно 2n. Таким образом, временная сложность этого алгоритма составляет O(2n). (Пространственная сложность составляет только O(n), поскольку перебор вариантов присваивания происходит по принципу поиска в глубину.) Ниже будут показаны алгоритмы, которые являются гораздо более эффективными на практике. К сожалению, каждый известный алгоритм логического вывода для пропозициональной логики в худшем случае имеет сложность, экспоненциально зависящую от размера ввода. Мы не можем рассчитывать на то, что наши алгоритмы будут действовать лучше, поскольку задача получения пропозиционального логического следствия является ко-NP-полной.