Содержание
- 2. Доведення. Нехай існує скінченна супе-речлива множина S′ основних прикладів диз’юнктів S. Так як кожна інтерпретація I
- 3. Приклад (а). Нехай S = {P(x), ¬P(f(x))}. Існує суперечлива множина основних прик-ладів диз’юнктів S′ = {P(f(a)),
- 4. Приклад. Нехай S = {¬P(x,y,u)∨¬P(y,z,v) ∨ ¬P(x,v,w)∨ P(u,z,w), ¬P(x,y,u)∨ ¬P(y,z,v)∨ ¬P(u,z,w)∨ P(x,v,w), P(g(x,y), x, y), P(x,
- 5. Застосування теореми Ербрана Теорема Ербрана для доведення супереч-ливості множини диз’юнктів припускає процедуру спростування. Це означає, що
- 6. Одним із перших використав цю ідею Гілмор. Але метод Гілмора виявився неефек-тивним. Більш ефективний метод, що
- 7. Так як H0 = {a}, H1= {a, g(a), h(a,a), k(a,a,a),e(a),f(a,a)}, . . . . . .
- 8. Тому виникла потреба в створенні іншого методу, в якому не потрібно було б породжу-вати множини основних
- 9. Метод резолюцій для логіки висловлювань Розглянемо наступні диз’юнкти: С1: P C2: ¬P∨Q. Df. Якщо А –
- 10. Викреслюючи контрарну пару із С1 і С2 одержимо дизюнкт: С3: Q. Узагальнюючи це правило, одержимо наступне
- 11. Приклад. Розглянемо наступні дизюнкти: С1: P∨Q, C2: ¬P∨Q. Диз’юнкт С1 містить літеру Р, контрарну літері ¬Р
- 12. Приклад. Розглянемо диз’юнкти С1: ¬P∨Q∨R, C2: ¬Q∨S. Резольвента С1 і С2 є ¬P∨R∨S. Приклад. Розглянемо диз’юнкти
- 13. Важливою властивістю резольвенти є те, що Теорема. Резольвента С диз’юнктів С1 і С2 є логічним наслідком
- 14. Припустимо спочатку, що L – фальшива в I. Тоді C′1повинен бути істинним в I. Отже, резольвента
- 15. Df. Нехай S – множина диз’юнктів. Резолютивне виведення С із S є така скінчен-на послідовність C1,
- 16. Далі множину диз’юнктів будемо запису-вати в стовпчик. Приклад. Для множини (1) P∨Q, (2) ¬P∨Q, (3) P∨¬Q,
- 17. Отже, ٱ – логічний наслідок S. Далі ми сформулюємо правило резолюцій для логіки першого порядку. Також
- 18. Підстановка і уніфікація Для застосування правила резолюцій суттєвим є наявність контрарних літер в різних диз’юнктах. Для
- 19. Не існує ніякої літери в С1, контрарної літері в С2. Однак, якщо ми підставимо f(a) замість
- 20. В загальному випадку, якщо підставити f(x) замість х в С1, то одержимо С1*: P(f(x)) ∨ Q(f(x)).
- 21. Диз’юнкт С3 теж будемо називати резоль-вентою С1 і С2. Одержання резольвенти потребує підста-новки замість змінних. Тому
- 22. Приклад. Наступні дві множини є підстановками: {f(z)/x, y/z}, {a/x, g(y)/y, f(g(b))/z}. Df. Нехай θ = {t1/v1,
- 23. Df. Нехай θ = {t1/x1, …, tn/xn} і λ = {u1/y1, …, um/ym} – дві підстановки.
- 24. Приклад. Нехай θ = {t1/x1, t2/x2} = {f(y)/x, z/y}, λ = {u1/y1, u2/y2 , u3/y3} =
- 25. Зазначимо, що композиція підстановок асоціативна, тобто (θ°λ)°μ = θ°(λ°μ) і ε°θ = θ°ε для всіх θ,
- 26. Df. Множина {E1, …, Ek} уніфікується, якщо для неї існує уніфікатор. Df. Уніфікатор σ для множини
- 27. Алгоритм уніфікації Далі буде приведений алгоритм для зна-ходження найбільш загального уніфікатора для скінченної множини виразів, що
- 28. Для P(a) і P(x) неузгодженість – це мно-жина {a, x}. Замінивши х на а ми позбудемо-ся
- 29. Приклад. Якщо W = {P(x, f(y,z)), P(x,a), P(x, g(h(k(x))))}, то перша позиція, в якій не всі
- 30. Алгоритм уніфікації Крок 1. k =0, Wk=W, σk= ε. Крок 2. Якщо Wk – одиничний диз’юнкт,
- 31. Крок 4. Нехай σk+1 = σk{tk/vk} і Wk+1 = Wk{tk/vk}. (Зазначимо, що Wk+1 = Wσk+1). Крок
- 32. 2. Множина неузгодженостей D0 = {a, z}. В D0 існує змінна v0 = z, яка не
- 33. 6. Нехай σ2 = σ1°{t1/v1} = {a/z}°{f(a)/x} = {a/z, f(a)/x}, W2 = W1 {t1/v1} = {P(a,
- 34. 8. Нехай σ3 = σ2°{t2/v2} = {a/z, f(a)/x}°{g(y)/u} = {a/z, f(a)/x, g(y)/u}, W3 = W2 {t2/v2}
- 35. Приклад. Знайти найбільш загальний уніфікатор для W = {Q(f(a), g(x)), Q(y,y)}. 1. σ0=ε і W0=W. 2.
- 36. 4. W1 – не одиничний дизюнкт. Множина неузгодженостей D1 для W1: D1 = {g(x), f(a)}. 5.
- 37. ньої. Теорема (уніфікації). Якщо W – скінчен-на непуста множина виразів, яка уніфікуєть-ся, то алгоритм уніфікації завжди
- 38. Метод резолюцій для логіки першого порядку Ввівши алгоритм уніфікації, можна роз-глянути метод резолюцій для логіки преди-катів.
- 39. Приклад. Нехай С=P(x)∨P(f(y))∨¬Q(x). Тоді перша і друга літери мають найбільш загальний уніфікатор σ = {f(y)/x}. Отже,
- 40. Приклад. Нехай С1= P(x)∨Q(x) і C2 = ¬P(a) ∨ R(x). Так як х входить в С1
- 41. Df. Резольвентою диз’юнктів С1 і С2 є одна із наступних резольвент: 1. Бінарна резольвента С1 і
- 42. Отже, правило резолюцій є правило виве-дення, яке породжує резольвенти для множи-ни диз’юнктів. Воно більш ефективне, ніж
- 43. Приклад. Показати, що внутрішні різно-сторонні кути, утворені діагоналлю трапеції, рівні. Аксіоматизуємо це твердження. Нехай T(x,y,u,v) означає,
- 44. Тоді будемо мати наступні аксіоми: А1. (∀x)(∀y)(∀u)(∀v)(T(x,y,u,v)→ P(x,y,u,v)) (визначення трапеції), А2. (∀x)(∀y)(∀u)(∀v)(P(x,y,u,v)→ E(x,y,v,u,v,y)) (внутрішні різносторонні кути
- 45. Отже, треба показати, що ¬(A1∧A2∧A3 → E(a,b,d,c,d,b)) є суперечливою. Для цього перетворимо цю формулу до стандартного
- 46. 1. ¬T(x,y,u,v)∨ P(x,y,u,v), 2. ¬P(x,y,u,v)∨ E(x,y,v,u,v,y), 3. T(a,b,c,d), 4. ¬E(a,b,d,c,d,b), 5. ¬P(a,b,c,d) (резольвента 2,4), 6. ¬T(a,b,c,d)
- 47. Теорема (повнота методу резолюцій). Множина S диз’юнктів суперечлива тоді і тільки тоді, коли існує виведення пустого
- 48. Таким чином, маємо: 1. ¬P∨S, 2. ¬S∨U, 3. P, 4. ¬U, 5. S (резольвента 3,1), 6.
- 49. Приклад. Розглянемо формулу ((∀x)(C(x)→(W(x)∧R(x))) ∧ (∃x)(C(x)∧O(x)) → (∃x)(O(x)∧R(x)). Покажемо, що вона істинна. Для цього заперечення цієї
- 50. Ця множина диз’юнктів суперечлива. Дійсно, за методом резолюцій будемо мати: 6. R(a) (резольвента 3,2), 7. ¬R(a)
- 51. Аксіоматизація має вигляд: (∀y)(S(y)→C(y)) → (∀x)((∃y)(S(y)∧V(x,y)) → (∃z)(C(z) ∧ V(x,z))) Стандартна форма для заперечення твердження є
- 52. Доведення завершується наступним чином: 5. С(b) (резольвента 1,2), 6. ¬V(a,b) (резольвента 5,4), 7. (резольвента 6,3).
- 53. Стратегії методу резолюцій Необмежене застосування методу резо-люцій може викликати генерацію великої кількості диз’юнктів. Наприклад, припустимо, що
- 54. Виконання методу резолюцій для цієї множини полягає в побудові всіх можливих резольвент множини S першого рівня,
- 56. Скачать презентацию