Сведение формул к предложениям

В методе резолюции используется стандартная форма формул, которая называется предложением. Предложение – это бескванторная дизъюнкция литералов. Любая формула исчисления предикатов может быть преобразована в множество предложений следующим образом (для обозначения способа преобразования формул используется знак Þ):

1) Элиминация импликации.

Преобразование . После первого этапа формула содержит только `,Ú, Ù,", $.

2) Протаскивание отрицаний.

Преобразования , , , , ` .

После второго этапа формула содержит отрицания только перед атомами.

1) Разделение связанных переменных.

Преобразование , где Q ₁ Q ₂– любые кванторы. После третьего этапа формулы не должны содержать случайно совпадающих переменных.

2) Приведение к предваренной форме.

Преобразование , где Q – любой квантор. После этого этапа формула находится в предваренной форме.

3) Элиминация кванторов существования.

Преобразование

где: a ₁ – новая предметная константа, f – новый функтор, а – произвольные кванторы. После этого этапа формулы содержат только кванторы всеобщности.

4) Элиминация кванторов всеобщности.

Преобразование .

После этого этапа формулы не содержат кванторов.

5) Приведение к конъюнктивной нормальной форме.

Преобразования:

После седьмого этапа формулы находятся в КНФ.

6) Элиминация конъюнкций.

Преобразование .

После восьмого этапа формула распадается на множество предложений.

Теорема:Если Г - множество предложений полученных из формулы S, то S является противоречием, тогда и только тогда множество Г не выполнимо. Множество формул Г невыполнимо – это означает, что множество Г не имеет модели, т.е. не существует такой интерпретации, в которой все формулы Г имели бы истинное значение.