Доказательство (Для случая L.) Г, ┐S├ F Г &┐S F - тавтология. Но

Г &┐ S F = ┐(Г&┐ S) F = ┐(Г&┐ S) = ┐Г S = Г S.

Имеем: Г S — тавтология Г ├ S.

Пустая формула не имеет никакого значения ни в какой интерпретации, в частности, не является истинной ни в какой интерпретации и, по определению, является противоречием. В качестве фор­мулы F при доказательстве от противного по методу резолюций принято использовать пустую формулу.

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

 

1. Элиминация импликации. Преобразование: А В ┐ А В. После первого этапа формула содержит только ┐, &, , , , .

2. Протаскивание отрицаний. Преобразования: ┐ x А x ┐ А, ┐ x A x ┐ А, ┐┐ A A, ┐ (A B) ┐ A & ┐ В, ┐ (A & B) ┐ A ┐ В. После второго этапа формула содержит отрицания только перед атомами.

3. Разделение связанных переменных. Преобразование:

Q ₁ x A(... Q ₂ x B(... x...)...) Q ₁ x A(... Q ₂ y B(... y...)...),

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

4. Приведение к предваренной форме. Преобразования:

Q x A B Q x (A B), Q x A&B Q x (A&В),

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

5. Элиминация кванторов существования (сколемизация). Преобразования:

x ₁ Q ₂ x ₂ ... Q_n x_n A(x ₁, x ₂ , ...,x_n) Q ₂ x ₂ ... Q_n x_n A(a, x ₂ , ...,x_n),

x ₁ ... x_{i- 1} x_i Q_{i+ 1} x_{i+ 1}... Q_n x_n A(x ₁,..., x_i, ...,x_n)

x ₁ ... x_{i- 1} x_i Q_{i+ 1} x_{i+ 1}... Q_n x_n A(x ₁,..., f(x ₁ ,..., x_{i- 1} ), ...,x_n)

где а — новая предметная константа, f — новый функтор, a Q ₁, Q ₂,..., Q_n — любые кванторы. После пятого этапа формула содержит только кванторы всеобщности.

6. Элиминация кванторов всеобщности. Преобразование: x А(х) А(х). После шестого этапа формула не содержит кванторов.

7. Приведение к конъюнктивной нормальной форме. Преобразование:

A (B&C) (A B)&(A C), (A&B) C (A C)&(B C).

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

8. Элиминация конъюнкции. Преобразование: A&В А, В. После восьмого этапа формула распа­дается на множество предложений.

Не все преобразования на этапах 1-8 являются логически эквивалентными.

Теорема 4.21. Если Г — множество предложений, полученных из формулы S, то S является проти­воречием тогда и только тогда, когда множество Г невыполнимо.

Доказательство. В доказательстве нуждается шаг 5 — сколемизация. Пусть

F= x ₁ ... x_{i- 1} x_i Q_{i+ 1} x_{i+ 1}... Q_n x_n A(x ₁,..., x_n).

Положим

F': = x ₁ ... x_{i- 1} x_i Q_{i+ 1} x_{i+ 1}... Q_n x_n A(x ₁,..., f(x ₁ ,..., x_{i- 1} ),

x_i+1,...,x_n).

Пусть F — противоречие, a F' — не противоречие. Тогда существует интерпретация I и набор зна­чений s = (a ₁,..., a_{i- 1}, a_{i+ 1},..., a_n) такой что (F') = И. Положим a_i:= f(a ₁,..., a_{i- 1} ), s ₁:= (a ₁,..., a_{i- 1}, a_i, a_{i+ 1},..., a_n). Тогда (F) = И и F — выполнимая формула.

 

Множество формул Г невыполнимо — это означает, что множество Г не имеет модели, то есть не существует интерпретации, в которой все формулы Г имели бы значение И.