Параграф
посвящен доказательству теоремы 4.3. Напомним ее формулировку.
Теорема. Множество дизъюнктов S невыполнимо тогда и только
тогда, когда из S
выводим пустой дизъюнкт.
Доказательство. Пусть множество
дизъюнктов S
невыполнимо и B={A1,A2,…,An,…} –
эрбрановский базис для S.
Рассмотрим полное семантическое дерево Т, изображенное на рис.4.8.
Рис. 4.8
По теореме Эрбрана Т содержит конечное замкнутое
семантическое поддерево Т/. Если Т/ состоит только из корня, то □ÎS и поэтому □ выводим из S. Предположим, что Т/ состоит не только из корня. Тогда Т/ имеет вершину v, потомки v1 и v2 которой являются максимальными опровергающими для
множества S
вершинами. Пусть
I(v)={L1, L2,…, Lk},
I(v1)={L1, L2,…,Lk,
Ak+1},
I(v2)={L1, L2,…,
Lk, ØAk+1}. |
Существует дизъюнкт D1ÎS такой, что его основной пример D1/ опровергается в I(v1), и существует дизъюнкт D2ÎS такой, что его основной пример D2/ опровергается в I(v2). Так как дизъюнкты D1/ и D2/ не опровергаются в I(v), то D1/ содержит ØAk+1, а D2/ – Ak+1. Применим к D1/ и D2/ правило резюлюций, отрезая литералы ØAk+1 и Ak+1, получим дизъюнкт D/:
D/=(D1/ – ØAk+1)È(D2/ – Ak+1).
Отметим, что дизъюнкт D1/ – Ak+1 ложен в I(v), поскольку в противном случае, D1/ был бы истинен в I(v1). Аналогично заключаем, что D2/ – Ak+1 ложен в той же интерпретации I(v).
Отсюда следует, что D/ ложен при I(v).
По лемме о подъеме (теорема 4.4)
существует дизъюнкт D, который является резольвентой дизъюнктов D1 и D2. Ясно, что D опровергается в I(v). Рассмотрим множество дизъюнктов SÈ{D}. Замкнутое семантическое
дерево T//
для этого множества дизъюнктов можно получить вычеркиванием некоторых вершин (и
идущих в них дуг) дерева T/.
А именно, в дереве T/
вычеркиваем все дуги и вершины, которые лежат ниже первой вершины, где дизъюнкт
D/
ложен. Полученное таким образом дерево T//
содержит меньше вершин, нежели дерево T/, так как v1,v2ÏT//.
Применим
описанный выше процесс к T//,
мы получим резольвенту дизъюнктов из SÈ{D}.
Расширим множество SÈ{D} за счет этой резольвенты,
придем к конечному замкнутому дереву с меньшим числом вершин, нежели T//.
В конце концов, получим замкнутое семантическое дерево, состоящее только из
корня. Это возможно, лишь в случае, когда множество S, расширенное резольвентами, содержит
пустой дизъюнкт, Следовательно, □ выводим из S. Необходимость условия
теоремы доказана.
Докажем
достаточность. Пусть пустой дизъюнкт выводим из S, и D1,D2,…,Dn=□
– вывод из S.
Предположим, что S
выполнимо в некоторой интерпретации. Тогда, поскольку правила резолюций и
правило склейки сохраняют истинность, то все дизъюнкты вывода, в том числе и
пустой, являются истинными в этой интерпретации. Полученное противоречие
доказывает, что S
невыполнимо.
Теорема доказана.
|