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

Первым понятием является логическая эквивалентность: два высказывания, α и β, являются логически эквивалентными, если они истинны в одном и том же множестве моделей. Это утверждение записывается как. Например, можно легко показать (с помощью истинностных таблиц), что высказывания логически эквивалентны; другие эквивалентности приведены в листинге 7.4. Они играют в логике практически такую же роль, какую арифметические равенства играют в обычной математике. Альтернативное определение эквивалентности является следующим: для любых двух высказываний α и β тогда и только тогда, когда (Еще раз напоминаем, чтоозначает логическое следствие.)

Листинг 7.4. Стандартные логические эквивалентности. Символы α, β и γ обозначают произвольные высказывания пропозициональной логики

Вторым понятием, которое нам потребуется, является допустимость. Высказывание допустимо, если оно истинно во всех моделях. Например, высказывание является допустимым. Допустимые высказывания известны также под названием тавтологий — они обязательно истинны и поэтому избыточны. Поскольку высказывание True является истинным во всех моделях, то любое допустимое высказывание логически эквивалентно True,