2.   Логический вывод с использованием хорновских выражений может осуществляться с помощью алгоритма прямого логического вывода и обратного логического вывода, которые рассматриваются ниже. Оба эти алгоритма являются очень естественными в том смысле, что этапы логического вывода являются для людей очевидными и за ними можно легко проследить.

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

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

Алгоритм прямого логического вывода PL-FC-Entails? (KB, q) определяет, следует ли единственный пропозициональный символ q (запрос) из базы знаний, представленной в форме хорновских выражений. Он начинает работу с известных фактов (положительных литералов) в базе знаний. Если известны все предпосылки некоторой импликации, то ее заключение добавляется к множеству известных фактов. Например, если известно, что имеют место фактыи Breeze, а в базе знаний имеется выражение, то к ней можно добавить факт . Этот процесс продолжается до тех пор, пока к базе знаний не добавляется запрос q или становится невозможным осуществление дальнейшего логического вывода. Этот подробный алгоритм приведен в листинге 7.6; главное, что следует о нем помнить, — то, что он действует за время, определяемое линейной зависимостью.

Листинг 7.6. Алгоритм прямого логического вывода для пропозициональной логики. В списке agenda ("повестка дня") отслеживаются символы, в отношении которых известно, что они истинны, но которые еще не "обработаны". В таблице count отслеживается информация о том, какое количество предпосылок каждой импликации еще не известно. Каждый раз, когда обрабатывается новый символ ρ из списка символов agenda, "стоящих на повестке дня", количество предпосылок в таблице count сокращается на единицу для каждой импликации, в которой появляется предпосылка р. (Такие импликации могут обнаруживаться за постоянное время, если индексация базы знаний KB выполнена должным образом.) После того как количество неизвестных предпосылок для некоторой импликации достигает нуля, все эти предпосылки становятся известными, поэтому заключение этой импликации может быть добавлено к списку agenda. Наконец, необходимо следить за тем, какие символы уже были обработаны; символ, выведенный логическим путем, не следует добавлять к списку agenda, если он уже был обработан ранее. Это позволяет избежать излишней работы, а также предотвратить возникновение бесконечных циклов, которые могут быть вызваны наличием таких импликаций, как