Примеры использования метода резолюций

Пример 9.7.

Предположим, что покупательная способность людей падает, если цены растут на товары и услуги. Положим также, что люди несчастны, когда их покупательная способность падает. Положим, что цены растут. Из этого можно заключить, что люди несчастны.

Применим следующие обозначения:

1. P — цены растут;

2. S — покупательная способность уменьшается;

3. U — люди несчастны.

В этом примере четыре утверждения:

Если цены растут, то покупательная способность падает;

Если покупательная способность падает, то люди несчастны;

Цены растут;

Люди несчастны.

Эти утверждения можно записать в виде следующих формул:

1. F1 : P ® S,

2. F2 : S ® U,

3. F3 : P,

4. F4 : U.

Преобразуем эти формулы в предложения:

(1) ùPÚS,

(2) ùSÚU,

(3) P,

(4) U.

Докажем путем опровержения, что U — логическое следствие из (1), (2) и (3). Отрицаем (4) и получаем следующее доказательство:

(1) ùPÚS,

(2) ùSÚU,

(3) P,

(4) ùU отрицание заключения,

(5) S резольвента (3) и (1),

(6) U резольвента (5) и (2),

(7)  резольвента (6) и (4).

Пример 9.8.

Допустим, что если Верховный Совет отказывается принять новые законы, то забастовка не будет закончена, если только она не длится более года и зарплата не повышается. Закончится ли забастовка, если Верховный Совет отказывается действовать и забастовка только что началась?

Применим следующие обозначения :

1. P — Верховный Совет отказывается действовать,

2. Q — забастовка заканчивается,

3. R — зарплата повышается,

4. S — забастовка длится более года.

Тогда приведенные выше утверждения можно представить следующими формулами :

F1 : (P ® (ùQÚ(RÙS))) — если Верховный Совет отказывается применять новые законы, то забастовка не будет закончена, если она не длится более года и зарплата не повышается,

F2 : P — Верховный Совет отказывается действовать,

F3 : ùS — забастовка только что началась.

Требуется доказать, что ùQ — логическое следствие F1ÙF2ÙF3. Отрицаем Q и преобразуем F1, F2 и F3 в предложения:

ùPÚùQÚR из F1,

ùPÚùQÚS из F1,

P из F2,

ùS из F3,

Q отрицание заключения.

Используя резолюции получим следующее доказательство :

(6) ùQÚS резольвента из (3) и (2),

(7) S резольвента из (6) и (5),

(8)  резольвента из (7) и (4).

Упражнения

9.1. Пусть истинно высказывание :

[("U)("V){R(U)®P(U,V)}]Ù[("W)("Z){Q(W,Z)®S(Z)}]ÙR(b)ÙùS(b)

Требуется преобразовать это высказывание в предложения и доказать истинность высказывания :

($X)($Y){P(X,Y)ÙùQ(X,Y)}.

9.2. В предложении A=P(X)ÚQ(Y)ÚR(Z) произвести замену

l={a/X, f(Y)/Y, X/Z}.

9.3. Рассмотрим высказывание логики предикатов :

Лошадь есть животное, поэтому голова лошади есть голова животного.

Пусть

H(X,Y) = X есть голова Y,

A(X) = X есть животное,

S(X) = X есть лошадь.

Посылка и заключение имеют вид :

("X)(S(X) ® A(X))

("X){($Y)([S(Y)ÙH(X,Y))] ® [($Z)(A(Z)ÙH(X,Z))]}

Доказать истинность заключения, используя резолюцию опровержения.

Показать все шаги преобразования заключения в дизъюнкты.