В логіці предикатів елементарним об`єктом, який має значення “істина”, є атомарна формула. Атомарна формула включає в себе символьні позначення предикату і термів, які відіграють роль аргументів цього предикату. В загальному випадку позначення предикату є ім`ям відношення, яке існує між аргументами.

Атомарна формула записується як позначення предикату і має наступний вигляд: Р(t1,t2,...,tn), де Р - позначення предикату, а t1,t2,...,tn - терми.

Число термів для кожного предикату фіксоване і називається його арністю. Терми визначаються наступним чином:

1)константний терм - терм;

2)змінний терм - терм;

3)якщо арність функціональної букви є n, а t1,t2,...,tn - терми, тоді f(t1,t2,...,tn) також терм.

Правильно побудована формула (ППФ) отримується в результаті комбінування атомарних формул за допомогою логічних зв`язок.

Символ позначає хибну замкнуту формулу і визначає поняття “протиріччя”. Так формула А означає хибність А, вона еквівалентна формулі А.

Серед формул можна виділити спеціальний клас формул - тотожньо істинні формули, які називають аксіомами. Приклад аксіоми:

А А.

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

1.4.Побудова теорії деякої області знань.

Побудова теорії деякої області знань включає в себе аналіз структури цієї області і вибір позначень, які визначають особливості даної структури. Потім будуються ППФ, які описують цю структуру. Множина ППФ є теорією цієї області знань, в якій кожна ППФ - аксіома.

Аналіз області знань включає виділення вагомих суттєвостей із цієї області. Дану множину називають областю інтерпретації. Далі визначаються найбільш важливі функції над елементами області інтерпретації, якщо такі існують, і значимі відношення між елементами області інтерпретації. По закінченню значимі відношення оформлюються синтаксично в вигляді аксіом.

Під функцією будемо розуміти відображення n елементів із області інтерпретації (де n - арність функції) на один з елементів цієї області.

Нехай областю є службові відношення між людьми в деякій фірмі. Областю інтерпретації буде наступна множина людей:

(Іван; Ігор, підлеглий Івана; Петро, підлеглий Івана; Микола, друг Петра).

На цій області можна виділити унарну функцію “друг”. Наприклад, друг (Петра) Микола.

Відношенням називають відображення n елементів із області інтерпретування на елемент множини (істина, хибність). В нашому прикладі можна виділити бінарне відношення “підлеглий”. Так, підлеглий (Івана, Ігор) матиме значення “істина”, а підлеглий (Ігор, Микола) прийме значення “хибність”.

Якщо в деякому конкретному випадку аргументів відношення буде істинним, тоді кажуть що відношення справджується.

Після фіксації області інтерпретування переходять до вибору позначень елементів області: констант, функцій, відношень. Відмітимо, що функція сама по собі не може мати значення - його може мати тільки конкретне використання функції. Аналогічне можна сказати і про відношення.

Проілюструємо це на нашому прикладі.

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

Значенням a буде Іван.

Значенням b буде підлеглий Івана Ігор.

Значенням с буде підлеглий Івана Петро.

Функцію “друг” позначимо f, тоді семантика цієї функції визначиться:

Значенням f(c) буде Микола.

Якщо позначимо через Р введене нами відношення “підлеглий”, тоді його семантика виразиться:

Значенням P(a,b) буде істина.

Значенням P(b,a) буде істина.

Значенням P(c,a) буде істина.

Значенням P(a,c) буде істина.

Значенням P(b,c) буде хибність.

Значенням P(c,b) буде хибність.

Значенням P(b,f(c)) буде хибність.

Значенням P(f(c),b) буде хибність.

Значенням P(a,f(c)) буде хибність.

Значенням P(f(c),a) буде хибність.

Значенням P(c,f(c)) буде хибність.

Значенням P(f(c),c) буде хибність.

Із даних атомарних формул маємо можливість будувати ППФ.

Інтерпретація, яка робить ППФ істиною називається моделлю цієї ППФ. Аналогічно визначається і модель теорії. Про ППФ, або ж теорію, яка приймає значення істина хоча б на одній інтерпретації, кажуть, що вона задовільна. Якщо ППФ, або ж теорія є хибною на всіх інтерпретаціях, тоді її називають незадовільною або ж непослідовною.

1.5.Від формальної логіки до логічного програмування.

В логіці предикатів існують методи доведення того, буде чи ні конкретна ППФ наслідком деякої теорії. Природньо виникає бажання автоматизувати таке доведення за допомогою предикату. В більшості підходів до цієї проблеми використовується процедура спростування. Розглянемо основні ідеї цієї процедури.

Із визначення тотожньої істинності і непослідовності можна зробити висновок, що ППФ буде тотожньо істинною тоді і тільки тоді, коли прибавлення в теорію заперечення даної ППФ перетворить цю теорію в непослідовну.

Теорія буде непослідовною, якщо в ній можливо вивести протиріччя наступного вигляду

А А.

Для вирішення згаданих задач дуже зручною є фразова форма логіки. Фразова форма логіки предикатів задає такий спосіб запису формул, який використовує тільки з`єднувачі типу , і .

Негативна або ж позитивна атомарна формула називається літералом. Кожна формула - множина літералів, які з`єднані символом . Негативні і позитивні літерали відповідно групуються. Схематично фраза має наступний вигляд:

Р1 Р2 ... Рn N1 N2 ... Nn, де P1 ... Pn - позитивні літерали, а N1... Nn - негативні. З другої сторони фразу можна розглядати як узагальнення поняття імплікації. Дійсно, якщо А і В атомарні формули, тоді формулу А В можна переписати і в такому еквівалентному вигляді: А В. Звідки отримаємо фразову формулу В А.

Фраза має наступну семантику. Всі позитивні атомарні формули виступають в ролі альтернативних заключень, а негативні - є необхідними умовами. Наприклад, А В С D зазначає що А і В будуть істиними тоді і тільки тоді, коли є істиними С і D.

Елементарна фраза має тільки один літерал. Теорія записується в вигляді множини фраз, які неявно з`єднані між собою символом . В літературі зустрічається і друга форма запису фрази за допомогою зворотньої стрілки, яка читається як “імплікується”. Так остання фраза може мати вигляд А, В С,