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

Подход, принятый в данном разделе, основан на проверке выполнимости логического высказывания, а не на доказательстве теорем. Мы будем отыскивать модели для пропозициональных высказываний, которые выглядят примерно так:

Такое высказывание должно содержать пропозициональные символы, соответствующие каждому возможному проявлению действия; модель, в которой выполняется это высказывание, должна присваивать значение true действиям, являющимся частью правильного плана, и false— другим действиям. Присваивание, которое соответствует неправильному плану, не будет моделью, поскольку окажется несовместимым с утверждением, что цель истинна. Если задача планирования неразрешима, то данное высказывание будет невыполнимым.