Для чего могут применяться допустимые высказывания? Из определения логического следствия можно вывести теорему дедукции, которая была известна еще в древней Греции:

Для любых высказываний а и β,, если и только если высказывание () является допустимым.

(В упр. 7.4 предлагается доказать эту теорему.) Алгоритм логического вывода, приведенный в листинге 7.3, может рассматриваться как проверка допустимости высказывания (). И наоборот, каждое допустимое высказывание в форме импликации описывает приемлемый вариант логического вывода.

Последним понятием, которое нам потребуется, является выполнимость. Некоторое высказывание выполнимо тогда и только тогда, когда оно истинно в некоторой модели. Например, приведенная выше база знаний, ( ), выполнима, поскольку существует даже не одна, а три модели, в которых она истинна (см. табл. 7.2). Если некоторое высказывание α является истинным в модели т, то для обозначения этого применяется выражение, что "т выполняет а", или что "m является моделью а". Выполнимость можно проверить, перебирая все возможные модели до тех пор, пока не будет найдена хотя бы одна из них, которая выполняет данное высказывание. Первой задачей в пропозициональной логике, для которой было доказано, что она является NP-полной, была задача определения выполнимости высказываний.

Многие задачи в компьютерных науках в действительно представляют собой задачи определения выполнимости. Например, во всех задачах удовлетворения ограничений, приведенных в главе 5, по сути требовалось найти ответ на вопрос о том, выполнимы ли данные ограничения при некотором присваивании. Кроме того, с помощью соответствующих преобразований по методу проверки выполнимости можно решать и задачи поиска. Безусловно, что понятия допустимости и выполнимости связаны друг с другом: высказывание α является допустимым тогда и только тогда, когда высказываниеневыполнимо, и наоборот, высказывание α является выполнимым тогда и только тогда, когда высказывание недопустимо. На этом основании может быть также получен следующий полезный результат:

( Высказываниеистинно, если и только если высказываниеневыполнимо.

Доказательство истинности высказывания β на основании истинности высказывания α путем проверки невыполнимости выражения точно соответствует стандартному математическому методу доказательства путем ^ приведения к абсурду (буквально, "доведение до абсурда" — reductio ad absurdum). Его также называют доказательством путем опровержения, или доказательством с помощью выявления противоречия. В этом методе доказательства принимается предположение, что высказывание β ложно, и демонстрируется, что такое предположение приводит к противоречию с известными аксиомами а. Подобное противоречие точно соответствует тому, что подразумевается под утверждением, что выражение невыполнимо.