Логика. логіка. Математична логіка та теорія алгоритмів

• Название: Математична логіка та теорія алгоритмів
• Анкор: Логика
• Дата: 15.05.2022
• Размер: 1.6 Mb.
• Имя файла: логіка.pdf
• Тип: Навчальний посібник; #530647
• страница: 12 из 18

Теорема 3.4.1 Якщо для диз’юнктів
2 1
, D
D
існує резольвента R(
2 1
, D
D
), то вона є логічним наслідком цих диз’юнктів:
)
,
(
|
,
2 1
2 1
D
D
R
D
D

Множина диз’юнктів
n
D
D
D
...,
,
,
2 1
називається невиконуваною, якщо формула
n
D
D
D
F




2 1
тотожно хибна.
Якщо можна встановити, що деяка формула F хибна, то можна відповісти, чи є логічне слідування





|
,...,
,
2 1
n
, оскільки для цього потрібно дослідити, чи буде формула










n
F
2 1
хибною.
Методом резолюцій називається послідовне отримання бінарних резольвент із заданих диз’юнктів та з усіх тих, що утворюються.
Застосовуючи метод резолюцій, можна отримати резольвенту, у якій не залишиться жодного літерала. Кажуть, що отримали порожній диз’юнкт □.
Теорема 3.4.2 (про повноту методу резолюцій). Множина диз’юнктів S невиконувана тоді і тільки тоді, коли у результаті застосування методу резолюцій до множини S отримується порожній диз’юнкт □.
Є багато різних процедур для реалізації методу резолюцій: локрезолюція, метод насичення рівня, стратегія викреслювання тощо.
У логіці предикатів для дослідження невиконуваності множини диз’юнктів потрібно провести додаткову процедуру уніфікації формул. Тут літералом є елементарна формула, терми якої можуть містити змінні, сталі або вирази із функціональних символів і термів.
)
),
(
,
(
b
y
f
x
P
,
__
__________
))
,
(
(
a
x
g
Q
))
,
(
,
,
(
2 1
2 1
x
x
f
x
x
S
- приклади літералів.
Підстановкою у літерали термів замість змінних можна отримати різні
частинні випадки (приклади) літерала. Наприклад, частинними випадком першого літерала можуть бути P(z,f(a), b), P(g(z ),f(c),b), P(с,f(a),b).
Останній частинний випадок називається атомом, бо не містить змінних.
Підстановку терма t замість змінної х позначають


/ x
t
Одночасно можна виконати кілька замін. їх групують у підстановку. Наприклад, перший частинний випадок отримано у результаті підстановки


y
a
x
с
/
,
/
1


другий
-


y
c
x
z
g
/
,
/
)
(
2


, третій


y
a
x
с
/
,
/
3


. У загальному випадку


k
k
x
t
x
t
x
t
/
/
,
/
2 2
1 1


де всі
k
x
- різні змінні,
k
t
- терми. Застосування підстановки

до літерала позначають Р
0
. Послідовне виконання двох підстановок
1

та
2

дає третю

81 2
1 3





.
Множина літералів {L
1
, L
2
,...L
n
} називається уніфікованою, якщо існує така підстановка

, що
)
(
)
(
)
(
2 1



n
L
L
L



Підстановка

називається
уніфікатором множини літералів {L
i
}. Уніфікатор

множини формул називається найзагальнішим, якщо для кожного уніфікатора

цієї множини існує підстановка

, що





Існує алгоритм уніфікації, який починає роботу з порожньої підстановки і крок за кроком знаходить множину неузгодженості в літералах і будує найзагальніший уніфікатор, якщо він є. Наприклад, для літералів
)
),
(
,
(
1
b
y
f
x
P
L 
та
)
),
(
,
(
1
b
b
f
a
P
L 
перша множина неузгодженості W1={x,a). Щоб ліквідувати неузгодженість, робимо підстановку

  
)
),
(
,
(
:
/
1 1
1
b
y
f
a
P
L
x
a




. Друга множина неузгодженості W2={y,b}. Після підстановки


y
b /
2


у новоутворений літерал
 
)
),
(
,
(
)
(
2 1
1
b
b
f
a
P
L



отримаємо однакові літерали.
Отже,
2 1





є найзагальнішим уніфікатором. Кожен елемент множини неузгодженості повинен бути термом або літералом. Якщо множина неузгодженості не містить змінних, то така множина літералів не уніфікується.
Нехай деякий диз’юнкт D містить літерали


K
L
L
L
,...,
,
2 1
для яких існує спільний уніфікатор. Тоді замість к літералів залишають один і така процедура називається склейкою.
Приклад 1. Знайти найзагальніший уніфікатор, якщо множина літералів уніфікується: a)


))
(
(
),
(
y
f
P
a
P
;
b)


))
(
(
),
(
a
f
P
x
P
;
c)


)
,
(
)),
(
,
(
y
x
P
x
f
a
P
Розв’язання. а)Для нескладних літералів алгоритм уніфікації очевидний.
Порівнюючи у літералах символи зліва направо, отримуємо множину неузгодженості


)
(
,
1 1
y
f
a
W 
. Вона не містить змінних, тому не можна здійснити жодної підстановки і множина літералів не уніфікується. b) Множина неузгодженості


)
(
,
1
a
f
x
W 
. Вона містить змінну х, тому можлива підстановка
}
/
)
(
{
1
x
a
f


і множина літералів набуде вигляду


))
(
(
)),
(
(
a
f
P
a
f
P
. Це однакові літерали, тому


x
a
f
/
)
(
1


є найзагальнішим уніфікатором.

82
c) У більш складних випадках бажано діяти за алгоритмом:
1. Вводимо порожню підстановку

. Початкова множина диз’юнктів


)
,
(
),
(
,
(
0
y
x
P
x
f
a
P
S 
не одиничний диз’юнкт, тому ще не отримали найзагальніший уніфікатор;
2. Для
0
S
множина неузгодженості


x
a
W
,
0

. Робимо підстановку


x
a /
1


 
:


)
,
(
),
(
,
(
)
(
1 0
1
y
a
P
a
f
a
P
S
S



- не одиничний диз’юнкт;
3. Для
1
S
множина неузгодженості


y
a
f
W
),
(
1

. Робимо підстановку


y
a
f
/
)
(
1 2


 
:

 

))
(
,
(
))
(
,
(
)),
(
,
(
)
(
2 0
2
a
f
a
P
a
f
a
P
a
f
a
P
S
S




. Множина диз’юнктів перетворилась на один диз’юнкт, тому


y
a
f
x
a
/
)
(
,
/
2


- найзагальніший уніфікатор.
Нехай є два диз’юнкти
1
D
і
2
D
і всі змінні у них різні. Диз’юнкт
1
D
, містить літерал
1
L
, а диз’юнкт
2
D
містить літерал
2
L
, причому існує уніфікатор

такий, що
 
 


2 1
L
L

. Бінарною резольвентою диз’юнктів
1
D
і
2
D
у логіці предикатів називається диз’юнкція літералів, які залишаються після викреслювання контрарних уніфікованих.
Перед побудовою резольвент спочатку виконують склейку у кожному диз’юнкті (якщо це можливо). У логіці предикатів теж справедлива теорема про повноту методу резолюцій. Наприклад, для перевірки логічного слідування





|
,...,
,
2 1
n
методом резолюцій потрібно:

Утворити формулу










n
F
2 1
. При цьому у кожній посилці та висновку змінні перейменувати, позначивши усі різними буквами, оскільки вони можуть мати різний зміст;

Знайти сколемівську стандартну форму цієї формули
*)
(
2 1
F
x
x
x
F
n
s




і записати її матрицю у кон’юнктивній нормальній формі
k
D
D
D
F
*
2 1



;

До множини диз’юнктів
n
D
D
D
,
2 1
застосувати метод резолюцій провівши, за необхідності, уніфікацію літералів. Якщо у результаті побудови всіх можливих резольвент отримується порожній диз’юнкт □, то множина диз’юнктів невиконувана, формули
S
F
і
F
тотожно хибні, отже, є логічне слідування.
Приклад 2. Перевірити за допомогою методу резолюцій, чи правильні наступні схеми логічних слідувань:

83
a)
)
)
(
)
(
(
x
P
x
M
x


,
))
(
)
(
(
x
M
x
S
x


⊨
)
)
(
)
(
(
x
P
x
S
x


; b)
)),
(
)
(
(
x
S
x
P
x


)
)
(
)
(
(
x
P
x
Q
x


⊨
)
)
(
)
(
(
x
S
x
Q
x


Розв’язання. a) З посилок та висновку утворимо формулу, яку потрібно перевірити на не виконуваність. Змінні у формулах в областях дії кванторів перейменуємо по різному, оскільки вони можуть мати різний зміст :
)
)
(
)
(
(
))
(
)
(
(
)
)
(
)
(
(
x
P
z
S
z
y
M
y
S
y
x
P
x
M
x
F









Зведемо формулу до випередженої нормальної форми:
)).
(
)
(
))
(
)
(
(
)
)
(
)
(
((
))
(
)
(
(
))
(
)
(
(
)
)
(
)
(
(
)
)
(
)
(
(
))
(
)
(
(
)
)
(
)
(
(
z
P
z
S
y
M
y
S
x
P
x
M
y
x
z
z
P
z
S
z
y
M
y
S
y
x
P
x
M
x
z
P
z
S
z
y
M
y
S
y
x
P
x
M
x
F




























Квантор існування можна винести першим, оскільки для кон’юнкції справедливий переставний закон. Це спростить запис сколемівської форми:
)).
(
)
(
))
(
)
(
(
)
)
(
)
(
((
a
P
a
S
y
M
y
S
x
P
x
M
y
x
F
s








Випишемо множину диз’юнктів:
(1)
)
(
)
(
x
P
x
M

;
(2)
)
(
)
(
y
M
y
S

;
(3)
)
(a
S
;
(4)
)
(a
P
a)
Далі проводимо уніфікацію літералів та утворюємо резольвенти, виписуючи їх за методом насичення рівня:
(5)
)
(
)
(
x
S
x
P

із (1), (1) після


y
x /
;
(6)
)
(a
M
із (1), (4) після


x
a /
;
(7)
)
(a
M
із (2), (3) після


y
a /
;
(8) із (6) і (7).
Оскільки отримали порожній диз’юнкт, то формула невиконувана, тому дане логічне слідування є правильним. Це один з правильних силогізмів
Арістотеля Celarent. З ілюстрації видно, що з даних посилок висновок є очевидним. b) Записуємо потрібну формулу та зводимо її до сколеміської форми:
).
(
)
(
)
)
(
)
(
(
))
(
)
(
((
));
(
)
(
(
)
)
(
)
(
(
))
(
)
(
(
)
)
(
)
(
(
)
)
(
)
(
(
))
(
)
(
(
a
S
a
Q
y
P
y
Q
y
x
S
x
P
y
x
F
z
S
z
Q
z
y
P
y
Q
y
x
S
x
P
x
z
S
z
Q
z
y
P
y
Q
y
x
S
x
P
x
F
x





























84
Випишемо множину диз’юнктів:
(1)
);
(
)
(
x
S
x
P

(2)
;
)
(
)
(
y
P
y
Q

(3)
);
(a
Q
(4)
).
(a
S
Утворюємо резольвенти: (5)
)
(a
P
із (2),(3) після


/ y
a
b)
Ніяких інших резольвент утворити не можна. Отже вивід порожнього диз’юнкта не існує. За теоремою про повноту методу резолюцій можна стверджувати, що висновок не є логічним наслідком даних посилок. З ілюстрації видно, що при правильності всіх посилок висновок може не виконуватись : не всі
Q
належать
S
. Більше того, можлива ситуація, коли всі
Q
належать
S
Приклад 3. Чи правильні міркування: а) Всі люди смертні. Сократ – людина. Отже він смертний; b) Всі, хто вміє обчислювати інтеграли, математики. Діти – не математики.
Деякі діти мають математичні здібності. Отже, дехто з тих, хто має математичні здібності, не обчислює інтегралів.
Розв’язання. а) Введемо предикати L(x)= «x – людина », C(x)= «x –
смертний» та елемент с=Сократ. Логічне слідування можна записати :
)
(
)),
(
)
(
(
c
L
x
C
x
L
x


⊨
).
(c
C
Далі:






)
(
)
(
))
(
)
(
(
c
C
c
L
x
C
x
L
x
F
)
)
(
)
(
))
(
)
(
((
s
F
c
C
c
L
x
C
x
L
x






Виписуємо диз’юнкти і резольвенти :
(1)
);
(
)
(
x
C
x
L

(2)
);
(c
L
(3)
).
(c
C
(4)
С(с) із (1), (2) після


;
/ x
c
(5)
)
(c
L
із (1), (3) після


;
/ x
c
(6)
□ із (2), (6).
Отже, міркування логічне і правильне.
c) Введемо предикати І(х) = «х – вміє обчислювати інтеграли», М(х) = «х -
математик», З(х) = «х – має математичні здібності», D(x) =«х - дитина». Тоді всі посилки та висновок можна записати :
))
(
)
(
(
),
)
(
)
(
(
)),
(
)
(
(
x
З
x
D
x
x
M
x
D
x
x
M
x
I
x






⊨
).
)
(
)
(
(
x
I
x
З
x


Далі :

85
)).
(
)
(
))
(
)
(
(
)
)
(
)
(
(
))
(
)
(
((
))).
(
)
(
(
))
(
)
(
(
)
)
(
)
(
(
))
(
)
(
((
))
(
)
(
(
))
(
)
(
(
)
)
(
)
(
(
))
(
)
(
(
)
)
(
)
(
(
))
(
)
(
(
)
)
(
)
(
(
))
(
)
(
(
a
З
a
D
t
I
t
З
y
M
y
D
x
M
x
I
t
y
x
F
t
I
t
З
z
З
z
D
y
M
y
D
x
M
x
I
t
y
x
z
t
I
t
З
t
z
З
z
D
z
y
M
y
D
y
x
M
x
I
x
t
I
t
З
t
z
З
z
D
z
y
M
y
D
y
x
M
x
I
x
F
s















































Виписуємо диз’юнкти і резольвенти :
(1)
);
(
)
(
x
M
x
I

(2)
;
)
(
)
(
y
M
y
D

(3)
);
(
)
(
t
I
t
З

(4)
);
(a
D
(5)
).
(a
З
(6)
)
(
)
(
y
D
y
I

із (1), (2) після


;
/ x
y
(7)
)
(
)
(
t
M
t
З

із (1), (3) після


;
/ x
t
(8)
)
(a
M
із (2), (4) після


;
/ y
a
(9)
)
(a
I
із (3), (5) після


;
/ y
a
(10)
)
(a
I
із (1), (8) після


/ x
a
(11) □ із (9), (10).
Тут не виписані зайві диз’юнкти за методом насичення рівня, оскільки порожній диз’юнкт отримується очевидно. Отже, дане міркування логічне і правильне.