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

Эта запись означает, что если даны любые высказывания в формеи а, то из них можно вывести высказывание β. Например, если дано (WumpusAhead

, то можно вывести высказывание Shoot.

Еще одним полезным правилом логического вывода является ^ правило удаления связки "И", в котором утверждается, что из конъюнкции можно вывести любой из ее конъюнктов:

Например, из высказыванияможно вывести высказывание WumpusAlive.

Рассматривая возможные истинностные значения α и β, можно легко показать, что правило отделения и правило удаления связки "И" являются непротиворечивыми не только применительно к данным примерам, но и ко всем возможным высказываниям. Это означает, что данные правила могут использоваться во всех конкретных случаях, в которых они могут потребоваться, вырабатывая непротиворечивые логические выводы без необходимости перебирать все модели.

В качестве правил логического вывода можно также применять все логические эквивалентности, приведенные в листинге 7.4. Например, из эквивалентности двухсторонней импликации и двух импликаций можно получить следующие два правила логического вывода (первое из них называется правилом удаления двухсторонней импликации):