Можно легко убедиться в том, что алгоритм прямого логического вывода является непротиворечивым: каждый этап логического вывода по сути представляет собой применение правила отделения. Кроме того, алгоритм прямого логического вывода является полным: в нем может быть получено каждое атомарное высказывание, которое следует из базы знаний. Проще всего в этом можно убедиться, рассмотрев заключительное состояние таблицы inferred (после того, как этот алгоритм достигает фиксированной точки, в которой становятся невозможными какие-либо новые этапы логического вывода). Эта таблица содержит значение true для каждого символа, выведенного логическим путем в течение этого процесса, и false— для всех других символов. Эта таблица может рассматриваться как логическая модель; более того, каждое определенное выражение в первоначальной базе знаний KB является истинным в данной модели. Чтобы убедиться в этом, предположим обратное, а именно, что некоторое выражениеиз базы знаний является ложным в этой модели. Тогда в этой модели выражениедолжно быть истинным и в ней же выражение b должно быть ложным. Но это противоречит нашему предположению о том, что алгоритм достиг фиксированной точки! Поэтому можно сделать вывод, что множество атомарных высказываний, полученное логическим путем к моменту достижения фиксированной точки, определяет модель первоначальной базы знаний КВ. Более того, любое атомарное высказывание д, которое следует из базы знаний KB, должно быть истинным во всех ее моделях, а также, в частности, в данной модели. Итак, любое высказывание д, которое следует из базы знаний, должно быть выведено логически данным алгоритмом.

Прямой логический вывод представляет собой пример применения общего понятия формирования логических рассуждений, управляемых данными, т.е. рассуждений, в которых фокус внимания вначале сосредоточен на известных данных. Прямой логический вывод может использоваться в любом агенте для получения заключений на основе поступающих результатов восприятия, часто даже без учета какого-либо конкретного запроса. Например, агент для мира вампуса может сообщать с помощью операции Tell результаты своих восприятий базе знаний с использованием инкрементного алгоритма прямого логического вывода, в котором новые факты могут добавляться к "повестке дня" для инициализации новых процессов логического вывода. У людей формирование рассуждений, управляемых данными, в определенной степени происходит по мере поступления новой информации. Например, находясь дома и услышав, что пошел дождь, человек, который собирался на пикник, может решить, что придется его отменить. Но такое решение вряд ли будет принято, если он узнает, что оказался мокрым семнадцатый лепесток самой крупной розы в саду его соседа; люди держат процессы прямого логического вывода под тщательным контролем, поскольку в противном случае их просто затопил бы поток логических заключений, не имеющих ничего общего с реальностью.