yandex rtb 1
ГоловнаЗворотній зв'язок
yande share
Главная->Математика і інформатика->Содержание->5.6. Примеры использования метода резолюций.

Математическая логика

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

Пример 1. Завершим рассмотрение примера 4.2 главы 4. ССФ посылок мы получили в 5.3: y((D(y)vL(a,y))&P(a)), xy(Q(y)v¬L(x,y)vP(x)).

Возьмем отрицание от следствия G: ¬y(t)(y) ¬Q(y)) = y¬(¬D(y)v¬Q(y)) = y(D(y)&Q(y)) - ПНФ. Элиминируем квантор : D(b)&Q(b) - ССФ.

Получили множество дизъюнктов:

1.      D(y)vL(a,y)))

2.      P(a))

3.      Q(y)v¬L(x, y)vP(x)

4.      D(b)

5.      Q(b)

6.      ¬L(x, b)vP(x)                                                   {b/y}, резольвента 5,3

7.      ¬L(a, b)                                                                        {a/x}, резольвента 2,6

8.      D(b)                                                                  {b/y}, резольвента 1,7

9.                                                                            резольвента 4,8

Пример 2. Посылка: "Каждый, кто хранит деньги, получает проценты". Заключение: "Если не существует процентов, то никто не хранит денег". Пусть S(x,y), М(х), J(х) и Е(х,у) означают "х хранит у", "х есть деньги", "х есть проценты" и "х получает у" соответственно. Тогда посылка

Записывается о виде

x(y(S(x,y)&M(y)) y(I(y)&E(x,y)))

а заключение - в виде

¬xI(x) xy(S(x,y) ¬M(y))

Переводя поселку в дизъюнкты, имеем                      

(1) ¬S(x,y)v¬ M(y)vI(f(x)),                     

(2) ¬S(x,y)v¬M(y)vE(x,f(x)).

Отрицание заключения:            

(3)I(z),                                              

(4)S(a,b),                                                                        

(5) M(b).

Дальнейшее доказательство на самом деле очень просто:

(6) ¬S(x,y)v¬M(y)                                                              из (3) и (1)

(7) ¬ M(b)                                                                           из (6) и (4)

(8)                                                                                       из (7) и (5)

Таким образом заключение доказано.

Пример 3 Посылка: "Студенты суть граждане." Заключение: "Голоса студентов суть голоса граждан."

Пусть S(x), С(х) и V(x,y) означают "х - студент", "х - гражданин" и "х -есть голос у" соответственно. Тогда посылка и заключение запишутся следующим образом:

y(S(y) C(y))                                                               (посылка),

x(y(S(y)& V(x,y) z(c(z)&V(x,z))                        (заключение).

Стандартная форма посылки есть

(1) ¬S(y)vC(y)

Так как

¬ (x(y(S(y)&V(x,y) z(C(z)&V(x,z)))= ¬x(y(¬S(y)v¬V(x,y)vz(C(z)&V(x,z))))=

¬(xyz(¬S(y)v¬V(x,y))v(C(z)&V(x,z))))= xyz((S(y)&V(x, y))&( ¬C(z)v¬V(x, z))),

имеем три дизъюнкта для отрицания заключения

(2) S(b)

(3) V(a,b),

(4) ¬C(z)v¬V(a,z)                                                  

Доказательство заканчивается следующим образом:    

(5) C(b)                                                                               {b/y}.      из(1)и(2),

(6) V(a,b)                                                                            {b/z}       из (5)и(4),

(7)                                                                                                       из(б)и(3).

Пример 4. Подобное доказательство логического следования позволяет формализовывать очень нетривиальные вещи, например, проверять некоторые философские рассуждения. Рассмотрим утверждение Лосева А.

Ф.5: "Вера в сущности своей и есть подлинное знание, и эти две сферы не только не разъединимы, но даже неразличимы ".

Доказательство Лосева заключается в следующем.

Верующий вериг в нечто. Вера свой предмет ясно отличает от всякого другою предмета. Тогда этот предмет определён. Но если он определен, он обладает признаками, отличающими его от всякого другого. Это значит, что мы знаем этот предмет. Мы знаем вещь, если по признакам можем отличить ?ё от всякого другого. Следовательно, вера и есть знание.

Пусть V(x,y) - и х верит в у ", С(х,у) - " х отличен от у", N(x,y) - м х шает у ".

1. Верующий верит в нечто.

xyV(x,y)

2. Верующий свой предмет отличает от всякого другого предмета.

xy(V(x,y) zC(y,z))

3. Мы знаем вещь тогда мы отличаем её от всякой другой вещи.

xyz{C(y,z) N(x,y))

4. Следовательно, "вера есть знание".

xy(V(x,y) N(x,y))

После   приведения   посылок   и   следствия   к   ССФ,   получим   множество дизъюнктов и резолютивный вывод:

1. V(x,f(x))                                                             - " х верит в предмет своей веры "

2.C(f(x),z)v¬V(x,f(x))                                            - " если х верит в f(x), to f(x) отличен от 2 "      3.N (x, f(x))v¬C(f(x),z)                                         - " x знает f(x), если может отличить его oт z "

4. V(b,y)                                                                 - «существует b который верит в у»

5. ¬N(b, y)                                                              -« b не знает у»

6. ¬V(b,f(b))                                                           -{b/x,f(x)/y}, резольвента (5,3)

7. ¬V(b,f(b))                                                           -  резольвента (6,2)

8.                                                                                     - резольвента (1,7)

 

 

 

36