Как начинался компьютер
Компьютерная революция
Двоичный код
Разработки военных лет
Интегральные микросхемы
Микрокомпьютер
Персоны
Сеть
Язык компьютера
Развитие ПО
Гибкие системы
Средства разработки
Информатика
Вычислительная наука
Операционные системы
Искусственный интеллект
Предыстория
Поиск
Знания и рассуждения
Логика
Робототехника
 

 
Эквивалентность и выполнимость Печать

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

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

α ≡ β тогда и только тогда, когда α |= β и β |= α

(Еще раз напоминаем, что |= означает логическое следствие.)

 

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

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

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

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

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

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

Высказывание α |= β истинно, если и только если высказывание (α^¬β) невыполнимо.

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