На головну

Аксіоматичні теорії першого порядку

  1.  II. Базові поняття теорії ймовірностей
  2.  II. еволюційні теорії
  3.  Quot; Гіпотези і теорії.
  4.  А (додаткова). Кілька слів про методологію науки. Принцип актуалізму, "Бритва Оккама" і презумпції. Перевірка теорії: верифікації та фальсифікації.
  5.  Адміністративний договір в зарубіжній адміністративно-правової теорії
  6.  аксіоматичні визначення

Задамо аксіоматичну теорію, використовуючи розширений мову предикатів:

1. Мова:

1). символи: службові: ®,, (,), ", $

предметні змінні: Z, y, x, ...

речові змінні: A, b, c, ...

функціональні символи: F, g, h, ...

символи предикатів: P, Q, R, ...

2). Терм:

Константа або змінна є терм.

якщо t1, t2, ... Tn- Терми, то f (t1, t2, ... Tn) - Теж терм.

3). Формула:

якщо t1, t2, ... Tn - Терми, то Р (t1, t2, ... Tn) - Формула.

Якщо P, Q - формули, то

(Р), P ® Q, P, "xP, $ xP - також формули.

2. Аксіоми:

1) -3) - відповідають схемам аксіом логіки висловлювань.

4) "x A (x) ® A (t)

5) A (t) ® $ x A (x)

де терм t вільний для x .

Терм t називається вільним для змінної x , Якщо ніяке вільне входження x в A не лежить в області дії ніякого квантора "y, де yзмінна, що входить в t .

Наприклад, терм y вільний для змінної x в A (x), але не вільний для змінної x в "y A (x). Терм f (x, z) вільний для x в" yA (x, y) ® B (x ), але не вільний для х в $ z "yA (x, y) ® B (x).

3. Правила виведення:

1). A, A ® B ?? B ( m.p.)

2) B ® A (x) ?? B ® "x A (x)

3) A (x) ® B?? $ x A (x) ® B

Вищенаведене обчислення називають ще обчисленням предикатів.

На практиці, як правило, до цих аксіом, званим логічними аксіомами

(Якщо вони описують логічну складову розглянутого "світу"), додають ще аксіоми, що описують конкретну "предметну область". Наприклад, закони управління автоматичним регулятором або роботом.

Такі аксіоми називаються власними аксіомами теорії, А самі теорії - аксіоматичними теоріями першого порядку або коротше, теоріями першого порядку.

Теорії першого порядку неповні, але, як правило, несуперечливі. (Хоча фахівців зі штучного інтелекту більше цікавлять "локально-суперечливі системи". Однак, чим більше такий інтерес, тим далі вони відходять від "класичної математичної логіки" з усіма наслідками, що випливають).

Говорячи про теоріях першого порядку можна хоча б не натякнути на існування теорій більш високих порядків. Так, наприклад, формула "P"x P(X) - вже не належить до мови теорій першого порядку через квантора "P.

2.5. метод резолюцій

Метод запропонований Дж. Робінсоном в 1965 році.

Метод резолюцій - аксіоматична теорія першого порядку, яка використовує доказ від протилежного, і, отже, не використовує аксіоматику числення предикатів (яка знаходиться в області тотожно істинних формул).

1. Мова методу резолюції - мова диз'юнктів :

2. Аксіоми тільки власні.

3. Правило виводу - резолюція

Важливе зауваження. Доведення коректності методу резолюції Дж. Робінсон виконав із залученням теорії моделей, розділу математичної логіки, який в даному курсі не розглядається. Тому ми скористаємося "правдоподібними" міркуваннями, якими рясніли перші книги з мови Пролог (Prolog). А мова Пролог (Програмування за допомогою Логіки) - мова, основний представник клас мов логічного програмування, Базується якраз на методі резолюції!

Правило виводу резолюція використовує розширений принцип силогізму і уніфікацію.

Традиційний силогізм: A ® B, B ® C ?? A ® C

Стосовно до диз'юнктивній записи можна уявити як

A U B A U B U D

B U C або "узагальнений" варіант B U C U E

       
   


A U C A U C U D U E

уніфікація:

Уніфікація теж суперечить здоровому глузду. Вона дозволяє замінити змінну х на терм t. Тобто замість змінної можуть бути підставлені константа або інша змінна (з тієї ж області), або функція, область значень якої збігається з областю визначення х.

a (const) ®xy (з тієї ж області)

f (z)

Висновок тут полягає в тому, що в систему додається заперечення формули (диз'юнкт!), Яку необхідно вивести. Висновок полягає в послідовному застосуванні резолюції до отримання порожнього диз'юнкт ?. Це буде, з точки зору інтерпретації, означатиме, що не існує ніякої моделі ( «світу»), в якій би була справедлива вихідна система законів (диз'юнктів). А якщо доказ виконується методом від противного, то значить первісна формула (диз'юнкт) дійсно виведена (і, отже, справедлива) в даній теорії.

Приклад 1: Можна сказати, що це прообраз або гранично спрощений варіант «системи штучного інтелекту».

Нехай мир описується двома аксіомами:

Миша всюди ходить за Оленою А1. "X (B (Л, x) ® B (M, x))

Лена в школі А2.B (Л, Ш)

Потрібно довести (відповісти на питання)

Де Міша? А3. $ Х B (M, x)?

Питання (доводить формулу з доданим знаком питання) $ х B (M, x)?

перетворимо в. $ Х B (M, x) (заперечення питання). далі

відсуває заперечення за квантор, виробляємо сколемізацію і

додаємо спеціальний «предикат відповіді», який буде акумулювати процес уніфікації). В результаті отримуємо диз'юнкт:

. B (M, x) U Відп (М, x)

Вся система (дві аксіоми і питання) буде складатися з трьох диз'юнктів:

Д1: B (Л, x) U B (M, x)

Д2: B (Л, Ш)

Д3: B (M, x) U Відп (M, x)

висновок:

Резолюція Д1-Д2 дає Д4: B (M, Ш)

Резолюція Д4-Д3 дає Д5: ?UОтв (M, Ш)

Тобто. предикат відповіді (при отриманні порожнього диз'юнкт) можна інтерпретувати як «Миша в школі». (Інтерпретація відповіді в системі штучного інтелекту залишається за людиною).

Приклад 2:

1. Якщо х є батьком y і y є батьком z, то х є прабатьком z.

А1. "Xyz (P (x, y) & P (y, z) ® P (x, z)

2. Кожна людина має свого батька.

A2. "Y $ xP (x, y)

3. Чи існують такі х і у, що х є прабатьком у?

$ XyP (x, y)?

Перетворимо аксіоми в диз'юнкт.

Д 1. OР (х, у) UOР (у, z) U P (x, z)

Д 2. P (f (y), y)

Д3.OP (x, y) U Відп (x, y)

Д1 - Д2: Д4: OР (у, z) U P (f (y), z)

Д4 - Д2: Д5: P (f (f (y)), y)

Д5 - Д3: Д6:? U P (f (f (х)), х)

Зауважимо, що кожна змінна має унікальне ім'я в межах одного диз'юнкт. Змінні, названі однаково в різних диз'юнкт - це різні змінні. Інтерпретація результату лежить на людині. будемо інтерпретувати

f (х) - як бути батьком х. Тобто f (f (х) - батько батька х. Отже, P (f (f (х)), х) - прабатько х - це батько батька х.

 




 Форми подання висловлювань |  перетворення висловлювань |  Перетворення СДНФ в СКНФ і навпаки. |  Мінімізація висловлювань методом Квайна |  Мінімізація за допомогою карт Вейча |  функціональна повнота |  логіка предикатів |  Основні равносильности для предикатів |  отримання диз'юнктів |  Аксіоматична теорія обчислення висловлювань |

© um.co.ua - учбові матеріали та реферати