Основные понятия и методы теории формальных систем. Волохович А.В. - 10 стр.

UptoLike

ВУЗ: 

НГТУ | Нижний Новгород

Составители: 

Рубрика: 

10
Принцип резолюции для логики высказываний
Легко проверяется, что формула
[(А
∨ В)&(B → C)]→ (A ∨ C) (1)
общезначима, т. е. является теоремой ИВ.
Лемма.
Пусть в КНФ K(X
1
, X
2
,…,X
n
) входят дизъюнкты D
1
и D
2
,причем D
1
представим в виде D
1
'
∨ X
i
, а D
2
– в виде D
2
'
∨
¬
X
i
.
Тогда логическим следствием входящих в КНФ утверждений
(дизъюнктов) является дизъюнкт D
1
'
∨ D
2
'
.
Действительно, дизъюнкт D
2
'
∨
¬
X
i
эквивалентен формуле X
i
→
D
2
'
. В формулу (1) вместо A подставим D
1
'
, вместо В - X
i
и вместо С
- D
2
'
. Получаем следующую теорему ИВ:
[(D
1
'
∨ X
i
)&( X
i
→ D
2
'
)]→ (D
1
' ∨ D
2
'
).
Так как утверждения D
1
'
∨
X
i
и X
i
→ D
2
'
входят в состав КНФ в
качестве логического следствия образующих КНФ K(X
1
, X
2
,…,X
n
)
дизъюнктов, получаем D
1
'
∨ D
2
'
. Лемма доказана.
Формула D
1
'
∨
D
2
'
называется резольвентой формул D
1
= D
1
'
∨
X
i
и
D
2
= D
2
'
∨ ¬ X
i .
Резольвента D
1
' ∨ D
2
'
- логическое следствие
дизъюнктов D
1
и D
2
.
Резольвентой однолитерных дизъюнктов X и
¬
X является
противоречивая формула (пустой дизъюнкт) .
Идея принципа резолюции заключается в проверке, выводим ли
из дизъюнктов, составляющих КНФ K(X
1
, X
2
,…,X
n
,), пустой
дизъюнкт. Вывод конструируется последовательным построением
резольвент. Выводимость из КНФ пустого дизъюнкта означает ее
противоречивость.
Пример 3.
Задана КНФ K(P,Q) = (Р ∨ Q) & (
¬
Р ∨ Q) & (Р ∨
¬
Q) &
(
¬ Р ∨ ¬ Q). Требуется доказать ее противоречивость,
В состав рассматриваемой КНФ входят четыре дизъюнкта:
1) Р
∨ Q;
2)
¬ Р ∨ Q;
3) Р
∨ ¬ Q;
4)
¬ Р
∨
¬ Q.
Строим следующие резольвенты (для каждой записываемой
резольвенты в скобках указываются номера исходных для нее
дизъюнктов):
5)Q (1,2);
6)
¬ Q (3,4);
7) (5,6). 
               Принцип резолюции для логики высказываний

     Легко проверяется, что формула

                   [(А ∨ В)&(B → C)] → (A ∨ C)                   (1)

общезначима, т. е. является теоремой ИВ.
       Лемма. Пусть в КНФ K(X 1 , X 2 ,…,X n ) входят дизъюнкты D 1 и D 2
,причем D 1 представим в виде D 1 ' ∨ X i , а D 2 – в виде D 2 ' ∨ ¬ X i .
Тогда логическим следствием входящих в КНФ утверждений
(дизъюнктов) является дизъюнкт D 1 ' ∨ D 2 ' .
       Действительно, дизъюнкт D 2 ' ∨ ¬ X i эквивалентен формуле X i →
D 2 ' . В формулу (1) вместо A подставим D 1 ' , вместо В - X i и вместо С
- D 2 ' . Получаем следующую теорему ИВ:

                  [(D 1 ' ∨ X i )&( X i → D 2 ' )] → (D 1 ' ∨ D 2 ' ).

    Так как утверждения D 1 ' ∨ X i и X i → D 2 ' входят в состав КНФ в
качестве логического следствия образующих КНФ K(X 1 , X 2 ,…,X n )
дизъюнктов, получаем D 1 ' ∨ D 2 ' . Лемма доказана.
    Формула D 1 ' ∨ D 2 ' называется резольвентой формул D 1 = D 1 ' ∨ X i и
D 2 = D 2 ' ∨ ¬ X i . Резольвента D 1 ' ∨ D 2 ' - логическое следствие
дизъюнктов D 1 и D 2 .
    Резольвентой однолитерных дизъюнктов X и ¬ X                является
противоречивая формула (пустой дизъюнкт) .
     Идея принципа резолюции заключается в проверке, выводим ли
из дизъюнктов, составляющих КНФ K(X 1 , X 2 ,…,X n ,), пустой
дизъюнкт. Вывод конструируется последовательным построением
резольвент. Выводимость из КНФ пустого дизъюнкта означает ее
противоречивость.
    Пример 3. Задана КНФ K(P,Q) = (Р ∨ Q) & ( ¬ Р ∨ Q) & (Р ∨ ¬ Q) &
( ¬ Р ∨ ¬ Q). Требуется доказать ее противоречивость,
    В состав рассматриваемой КНФ входят четыре дизъюнкта:
                     1) Р ∨ Q;
                     2) ¬ Р ∨ Q;
                     3) Р ∨ ¬ Q;
                     4) ¬ Р ∨ ¬ Q.
     Строим следующие резольвенты (для каждой записываемой
резольвенты в скобках указываются номера исходных для нее
дизъюнктов):
                     5)Q        (1,2);
                     6) ¬ Q (3,4);
                     7)         (5,6).



10

Страницы