Принцип резолюций

8.3.1. Принцип резолюций

Ранее я уже вскользь упоминал о том, что мы стараемся упростить синтаксис исчисления таким образом, чтобы уменьшить количество правил влияния, необходимое для доказательства теорем. Вместо дюжины.или более правил, которые используются при доказательстве теорем вручную, системы автоматического доказательства для фразовых форм используют единственное правило вывода — принцип резолюций, — впервые описанное Робинсоном ([Robinson, 1965]).

Рассмотрим следующий пример из исчисления высказываний. В дальнейшем прописными буквами Р, Q, R,... будут обозначаться отдельные фразы, а строчными греческими U, ф и £ — пропозициональные переменные, как и раньше.

Если U и ф представляют две произвольные фразы, которые можно представить в конъюнктивной нормальной форме, и

U={ U1, ..., Ui, ...., Um},

ф= {ф1..., фi.....,фn}, и

Ui, = ¬фi при 1[i[mm,1 [j [ n,

то новую фразу £ можно вывести из объединения U' и ф', где

U' = U¬{ Ui} и ф' = ф¬{ф,}.

Фраза £ = U' и ф' называется резольвентой шага резолюции, а U и ф являются родительскими фразами. Иногда говорят, что U и ф "сталкиваются" на паре дополняющих литералов Ui , и фj.

Мощность резолюции обеспечивается тем, что в ней суммируется множество других правил. Это станет очевидно после того, как обычные правила будут представлены в конъюнктивной нормальной форме.

В левой колонке табл. 8.1 перечислены наименования правил вывода, в средней показано, как они выглядят в обычных обозначениях, а в правой колонке — во фразовой форме. В каждой записи выражения в верхней части представляют схему предпосылок, а выражения в нижней части — схему заключений. Из этой таблицы видно, что каждое из цитированных выше пяти правил является одним из экземпляров резолюции!

Содержание раздела