Логічне і функціональне програмування

ЛОГІЧНІ І ФУНКЦІОНАЛЬНИЙ ПРОГРАМУВАННЯ

Введення

Метою логічного і функціонального програмування є висновок рішень і вони тісно пов'язані із завданнями, які розв'язуються в штучному інтелекті та експертних системах (ЕС). На початковому етапі розвитку систем штучного інтелекту (СІІ) і ЕС навіть виділився цілий клас спеціалізованих мов програмування: мови логічного і функціонального програмування.

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

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

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

Найбільш відомими мовами функціонального програмування є ЛИСП і Рефан, а логічного - Пролог. Однак, з розвитком мов програмування (зокрема, з появою об'єктно-орієнтованих мов) і баз даних область їх застосування звузилася. Так ЛИСП використовується як оболонка Автокад, а Рефан як засіб для побудови метамови і метакомпіляторов.

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

ЛИСП і Пролог свого часу були базовими для створення експертних систем. Тому, для того, щоб наочно уявити яке коло завдань вирішується за допомогою логічного та функціонального програмування, розглянемо завдання, що виникають в ЕС. Перш за все, це завдання прямого і зворотного висновку.

Прямий і зворотній висновок

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

Такі завдання часто записують у термінах продукційних систем представлення знань, в яких знання записуються у вигляді продукцій / правил, що мають вигляд:

Якщо <умова>, Те <висновок>.

Розглянемо спочатку побудова зворотного ланцюжка міркувань. Зворотній ланцюжок міркувань завжди починається зі слідства (частина Те правила). Якщо в правилах, що відносяться до проблемної області, не вдається знайти умовну частину з запущеними умовами, необхідно ввести додаткову інформацію. Ланцюжок означає процедуру логічного зв'язку ряду правил.

Для представлення таких завдань прийнято використовувати дерево рішень - спеціальну діаграму для подання можливих рішень. Дерево рішень складається з вершин двох типів. Вершини рішень, що містять питання, позначаються колами. Цілі або логічні висновки позначаються прямокутниками. Вершини нумеруються. Кожна вершина може мати не більше одного входу. Розглянемо найпростіший приклад з прийомом на роботу, часто використовуваний в літературі [1].

Дерево рішень будемо зберігати в наступній таблиці [2]:

Таблиця дерева рішень.

Для збереження результатів будемо використовувати таблицю виводу (в початковий момент таблиця порожня).

Таблиця виведення

Алгоритм

1. Визначити змінну логічного висновку та її значення.

2. Знайти перше входження цієї змінної в таблицю дерева рішень із заданим значенням і типом вершини «висновок». Якщо змінна не знайдена - невдача. Встановити змінну var = 1.

3. Вибрати вихідну по відношенню до отриманої вершині вершину. Якщо її нат, перейти до кроку 5. Якщо є, записати в таблицю виведення новий рядок зі значеннями полів № варіанту = var, Змінна = Дані з вихідної вершини таблиці дерева рішень, Значення = Дуга поточної вершини.

4. Зробити вихідну вершину поточної. Перейти до кроку 3.

5. Знайти наступне входження змінної виводу в таблицю дерева рішень. Якщо ні, кінець, інакше var = var + 1. Перейти до кроку 3.

Нехай відмовлено в прийомі на роботу. Тоді в ході виконання алгоритму таблиця виведення буде формуватися наступним чином.

Тут пропущена таблиця виведення на передостанньому етапі.

Механізм, заснований на прямий ланцюжку міркувань, функціонує наступним чином:

1. Вводиться умова.

2. Для кожної ситуації система шукає в базі даних (знань) правила, в умовній частині яких міститься відповідне умова.

3. Відповідно до констатуючої частиною (частиною ТО) кожне правило може генерувати нові ситуації, які додаються до вже існуючих.

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

Алгоритм CLS

Для побудови дерев рішень часто використовується алгоритм CLS. Цей алгоритм циклічно розбиває навчальні приклади на групи / класи відповідно до змінної, що має найбільший классифицирующую силу. Кожна підмножина прикладів (об'єктів), що виділяється такої змінної, знову розбивається на класи з використанням наступної змінної з найбільшою классифицирующей здатністю і т.д. Розбиття закінчується, коли в підмножині виявляються об'єкти лише одного класу. У ході процесу утворюється дерево рішень. Шляхи руху по цьому дереву з верхнього рівня на самі нижні визначають логічні правила у вигляді ланцюжків кон'юнкція.

Розглянемо наступний приклад. Проводиться антропологічний аналіз осіб людей двох національностей по 16 ознаками.

Х1 (голова) - кругла - 1, овальна - 0.

Х2 (вуха) - відстовбурчені - 1, притиснуті - 0.

Х3 (ніс) - круглий -1, довгий - 0.

Х4 (очі) - круглі - 1, вузькі - 0.

Х5 (лоб) - зі зморшками -1, без зморшок - 0.

Х6 (носогубная складка) - є - 1, ні - 0.

Х7 (губи) - товсті - 1, тонкі - 0.

Х8 (волосся) - є - 1, ні - 0.

Х9 (вуса) - ​​є - 1, ні - 0.

Х10 (борода) - є - 1, ні - 0.

Х11 (очки) - є - 1, ні - 0.

Х12 (родимка) - є - 1, ні - 0.

Х13 (метелик) - є - 1, ні - 0.

Х14 (брови) - підняті вгору - 1, опущені - 0.

Х15 (сережка) - є - 1, ні - 0.

Х16 (трубка) - є - 1, ні - 0.

Нехай є 16 об'єктів. Об'єкти з номерами 1 - 8 належать до першого класу, 9 - 16 до другого класу. Далі наводиться таблиця зі значеннями ознак для цих об'єктів.

Об'єкти для цієї таблиці (треба намалювати).

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

ЯКЩО А ТО В,

ЯКЩО (условіе1) І (условіе2) І ... І (умова N) ТО (умова N +1),

де умова i може бути Xi = C 1, Xi <C 2, Xi> C 3, C 4 <Xi <C 5 і т.д. Тут Xi - змінна, Cj - константа.

Так класифікація осіб у розглянутому прикладі може бути зроблена за допомогою чотирьох логічних правил:

1. ЯКЩО (голова овальна) І (є носогубная складка) І (є окуляри) І (є трубка) ТО (класс1).

2. ЯКЩО (очі круглі) І (лоб без зморшок) І (є борода) І (є сережка) ТО (класс1)

3. ЯКЩО (ніс круглий) І (лисий) І (є вуса) І (брови підняті вгору) ТО (класс2).

4. ЯКЩО (відстовбурчені вуха) І (товсті губи) І (немає родимки) І (є метелик) ТО (класс2).

Математична запис цих правил виглядає наступним чином:

Такі правила мають дві основні характеристики: точність і повноту.

Точність правила - це частка випадків, коли правило підтверджується, серед всіх випадків його застосування (частка випадків В серед випадків А).

Повнота - це частка випадків, коли правило підтверджується, серед всіх випадків, коли має місце зрозумілий результат (частка випадків А серед випадків В).

Правила можуть мати які завгодно поєднання точності та повноти. За винятком одного випадку, якщо точність дорівнює нулю, то дорівнює нулю і повнота, і навпаки.

Точне, але неповне правило: Люди смертні (А - людина, В - смертна).

Неточне, але повне правило: Студенти відвідують заняття (А - студент, В - відвідує).

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

Повернемося до прикладу.

На першому кроці визначається ознака з найбільшою дискримінує силою. Для цього визначається ставлення входження об'єктів у різні класи у відповідності зі значеннями різних ознак:

Тут однаковою і максимальною силою володіють відразу сім ознак: Х2, Х3, Х6, Х7, Х10, Х11, Х14, Х15. Тому випадковим чином вибираємо один з них у якості ведучого. Нехай це буде Х6. Від цієї ознаки відходить дві гілки. Перша для значення Х6 = 0, а друга - для Х6 = 1.

Для гілки Х6 = 0 остаточне рішення дає ознака Х10. Він приймає значення 1 на об'єктах 2 і 7 з першого класу і значення 0 на об'єктах 12, 13, 14 і 16 другого класу. Гілка Х6 = 1 влаштована значно складніше і вимагає додаткових розгалужень. У результаті отримуємо дерево.

Як випливає з малюнка дерево логічного висновку, що виросло з ознаки Х6 має 6 випадків. Тільки два з цих результатів має по чотири об'єкти (повнота 4 / 8). Один результат групує три об'єкти (повнота 3 / 8), один - два об'єкти (повнота 2 / 8) і три результати включають по одному об'єкту (повнота 1 / 8). Звідси, якість алгоритму не дуже високо, тому що має малу повнотою. Алгоритм, крім того, здатний приводити до якісних рішень тільки у випадку незалежних ознак.

Домашнє завдання

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

Комп'ютерне завдання

Реалізувати дерево рішень, прямий і зворотній висновок засобами Access. Для реалізації необхідно використовувати VBA. У Access 2000 за умовчанням встановлена ​​модель даних ADO (ActiveX Data Objects). Для установки MSDE, що відповідає моделі даних DAO, використовуваної в Access 97, необхідно використовувати інший файл установки. Необхідно вставити інсталяційний компакт диск і двічі клацнути на імені файлу SETUPSQL. EXE в папці \ Sql \ x 86 \ Setup.

Ієрархія ADO простіше ієрархії об'єктів моделі

Об'єкти ADO призначені для організації доступу до джерел даних, їх редагування і оновлення. Модель ADO включає в себе об'єкти, необхідні для виконання наступних завдань:

1. З'єднання з джерелом даних.

2. Створення об'єкта, що реалізує команди SQL.

3. Вказівка ​​стовпців, таблиць та значень як змінних параметрів у команді SQL.

4. Виконання команди SQL.

5. Збереження результатів виконання в хеш-кодуванні.

6. Створення віртуального представлення в хеш-кодуванні, щоб користувач міг сортувати, фільтрувати дані в БД і переміщатися по ній.

7. Редагування даних.

8. Оновлення джерела даних у відповідності з усіма змінами зробленими в хеш-кодуванні.

9. Фіксація або скасування змін, внесених в ході транзакції, і наступне закриття транзакції.

До класами об'єктів в моделі ADO відносяться:

• Connection - представляє середовище, в якому буде виконуватися обмін даними з джерелом даних. З'єднання має бути встановлено до початку виконання будь-яких інших операцій.

• Command - спосіб управління джерелом даних. Можна видаляти, додавати, оновлювати і зчитувати дані з джерела.

• Parameter - представляє змінні компоненти об'єкта Command. У командах часто необхідно вказувати допоміжні параметри, що уточнюють спосіб виконання команд. Параметри є змінюваними, так що перед виконанням команд їх можна модифікувати

• Recordset - служить локальним хешем даних, лічених з джерела даних.

• Field - представляє стовпець таблиці Recordset. Поле містить властивості визначають поле. Приклад таких властивостей - Type, Value.

• Error - повертає результат щоразу, коли в додатку виникає помилка. Кожен об'єкт Connection має окреме сімейство об'єктів Error.

• Property - визначає об'єкти Connection, Command, Field, Recordset. Кожен об'єкт ADO володіє набором властивостей, що задає об'єкт і керуючим його поведінкою.

• Collection - служить для об'єднання подібних об'єктів в групи.

Звернення до об'єктів ADO виглядає так:

ADODB. імя_об'екта.

При створенні нового проекту, Access 2000 завантажує тільки бібліотеку об'єктів ADO. Якщо необхідно працювати з DAO, додається бібліотека об'єктів DAO в діалозі Preferences редактора VB. Для відкриття VB Editor треба натиснути Alt + F 11. Діалог Preferences відкривається командою меню Tools> References. У цьому діалозі треба вибрати DAO 3.6 Object Library.

Для того щоб зв'язати об'єкт Recordset в моделі ADO з даними необхідно:

Dim rst As New ADODB.Recordset

rst.Open SQLVar, CurrentProject.Connection

Тут SQLVar символьна змінна, в якій визначається набір даних або як вираз SQL, або як ім'я таблиці. Наприклад, якщо необхідно відкрити таблицю з ім'ям Student, другий рядок буде виглядати:

rst. Open "Student", CurrentProject. Connection

У разі DAO необхідно створити об'єктну змінну rst типу Recordset без ADODB, а потім використовувати метод OpenRecordset:

Set rst = CurrentDB.OpenRecordset (SQLVar, dbOpenDynaset).

Тут необхідно бути акуратним, оскільки написання для об'єктів Recordset в обох моделях однаково.

Для переходу в обох моделях використовуються методи Move:

• rst. MoveFirst | MoveLast | MoveNext | MovePrevious | Move n - відповідно: Перейти до першого запису | до останньої | до наступного | до попередньої | на n записів

Метод Find використовується при пошуку в наборі записів, які відповідають тим або іншим умовам.

Переменная_ Recordset критерій, Пропустити Рядки, Напрямок Пошуку, Старт

Тут:

• критерій - строкове значення (обов'язково в лапках), що визначає ім'я стовпця (поля), оператор порівняння і шукане значення. Це єдиний обов'язковий параметр.

• Пропустити рядки - позначає число рядків, починаючи з поточної чи стартової позиції, яке необхідно пропустити перед початком пошуку.

• Напрямок пошуку визначає чи повинен пошук вестися у напрямку до кінця набору (adSearchForward) або до початку (adSearchBackward).

• Старт - закладка, що позначає початкове положення покажчика поточного запису при пошуку: adBookmarkFirst (1) - перший запис, adBookmarkLast (2) - останній запис, adBookmarkCurrent (0) - поточна запис.

Dim Rst As New ADODB.Recordset

Rst.Open "Student", CurrentProject.Connection

Rst.Find "Sgroup = 'АП 51'"

Rst. Close

Значення критерію може бути рядком, числом або датою. Якщо значення має тип дати, то воно полягає в #, наприклад, # 11/11/03 #.

При оновленні записів за допомогою Recordset. Open необхідно встановити значення декількох властивостей, що визначають набір даних. Найважливішими з цих властивостей є властивості LockType і CursorType.

LockType визначає право доступу до набору та приймає значення:

• AdLockReadOnly - об'єкт доступний тільки для читання (значення за замовчуванням).

• AdLockPessimistic - записи блокуються відразу після початку редагування по одній.

• AdLockOptimistic - встановлює блокування при виклику методу Update (використовуйте цей варіант).

• AdLockBatchOptimistic - дозволяє пакетне оновлення.

Властивість CursorType визначає тип курсора, застосовуваний в наборі даних. Його дія подібно визначення набору даних в моделі DAO. CursorType може приймати одноіз наступних значень:

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

• AdOpenKeySet - дозволяє вносити зміни в набір даних, але користувач бачить зміни, внесені ним самим.

• AdOpenDynamic - дозволяє вносити зміни. Користувач бачить всі результати змін. Найменш ефективний, але має найбільше можливостей. Тому використовуйте його.

• AdOpenStatic - набір являє собою статичну копію даних.

Редагування:

Rst.Open "Student", CurrentProject.Connection, adOpenDynamic, adLockOptimistic

Rst.MoveFirst

Rst ("YearEnter") = 2001

Rst.Update

Rst. Close

Оновлюється полі YearEnter першого запису.

Додавання запису:

Rst.Open "Student", CurrentProject.Connection, adOpenDynamic, adLockOptimistic

Rst.AddNew

Rst ("FIO") = "Петров І.І."

Rst ("YearEnter") = 2003

Rst.Update

Ret. Close

Видалення запису:

Rst.Open "Student", CurrentProject.Connection, adOpenDynamic, adLockOptimistic

Rst.MoveFirst

Rst.Delete adAffectCurrent

Rst.Update

Rst.Close

2. Математичні основи

Математичними основами індуктивного і дедуктивного виводу є математична логіка та її розвиток логіка предикатів першого порядку.

Логіка використовується для того, щоб доводити правильність або неправильність тих чи інших тверджень або висловлень. Це має велике значення при вирішенні завдань проектування і для інших обчислювальних завдань. Так штучний інтелект багато в чому спирається на гіпотезу символьних систем. Спрощено ця гіпотеза стверджує, що, організувавши величезну структуру взаємопов'язаних символів, що представляють реальні знання і складний набір символьних процесів, що дозволяє оперувати структурами з метою створення нових структур, можна створити машину, що працює також добре в сенсі інтелектуальної діяльності, як людина.

2.1 Алгебра висловлювань

Одним з основних понять логіки є поняття висловлювання, правильність або неправильність якого ми намагаємося визначити. Спробуємо визначити зміст цього терміна. Висловлюванням називають пропозиції, про які розумно говорити, розумно вважати, що вони є істинними або помилковими. Неуточненої понять «істинно» та «хибно» роблять поняття висловлювання розпливчастим. Проте, вводячи обмеження можна це поняття уточнити. Фрази «Підемо в кіно?», «Хай живе президент!» Не є висловленнями (як і будь-які запитання й оклику пропозиції). Фраза «Трикутник називається рівностороннім, якщо всі його сторони рівні» (як і будь-яке інше визначення) також не є висловлюванням. Фрази «2 * 2 = 4» і «3> 5» - висловлювання (перше справжнє, друге помилкове). Фраза «У повісті" Шинель "200755 літер» - висловлювання, але нам невідома його істинність. Фразу «Ця книга хороша» не слід відносити до висловлювань у традиційній логіці в силу невизначеності поняття «добрий».

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

З простих висловлювань з допомогою зв'язок можна будувати складні висловлювання, і тоді виникає задача визначення їх істинності в залежності від істинності простих висловлювань, його складових.

Зміну, в область значень якої входять тільки висловлювання (а точніше істінностние значення T, F) будемо називати висказивательной змінної (двійковій або булевої). У силу визначення областю значень цих змінних є двійковий алфавіт.

Функції від будь-якого кінцевого числа двійкових змінних, також здатні приймати лише два значення T і F, прийнято називати булевими функціями. Іноді такі функції називають переключательную, так як реалізують такі функції схеми здійснюють переключення вхідних каналів, подаючи на них сигнали, то одного, то іншого виду.

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

Для будь-якого n = 1, 2,. . . серед n - вимірних наборів можна ввести природну лексикографічну впорядкованість. Для цього поставимо у відповідність з F - 0, а з T - 1. Тоді набір перетвориться в послідовність 0 і 1. Такий набір вже можна розглядати як представлення цілого невід'ємного числа в двійковій системі числення. Наприклад, TTTF ® 1110 ® 14. Це число будемо називати номером набору. Ці набори називаються також кортежами або, використовуючи геометричну термінологію, крапками.

Остання назва пов'язана з тим, що є природна можливість ототожнювати різні n - мірні набори з вершинами n-мірного куба.

Природну впорядкованість наборів ми отримаємо, якщо розташуємо їх у порядку зростання номерів. Першим в такому розташуванні є нульовою набір, всі компоненти якого 0, останнім - набір, всі компоненти якого 1.

Звідси, набори розмірності n нумеруються числами від 0 до 2 ^{n -1.} А звідси зокрема випливає:

1. Мається на точності 2 ⁿ двійкових n-мірних наборів.

Неважко також підрахувати кількість різних булевих функцій від n змінних. Для кожного набору значень, незалежно від значень інших наборів, можна вибрати в якості значень функції T або F. Отже, прибуток кожного нового набору до області визначення булевої функції збільшує число різних булевих функцій рівно в два рази.

На одному наборі можна визначити дві різних булевих функції. На двох - ² 2 і т. д. Продовжуючи подібним чином і з урахуванням 1, отримаємо:

2. Є точно різних булевих функцій від n змінних.

Слід зазначити, що тут і далі до числа функцій від n змінних відносяться і такі функції f (x 1, x 2,..., Xn), які не залежать від тих чи інших змінних xi. Зокрема, серед функцій виявляться функції - константи (тотожна істина і тотожна брехня), які можна розглядати як функції від нуля змінних.

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

У теорії булевих функцій особливе значення мають функції однієї та двох змінних. Є всього = 4 різних функцій однієї змінної.

G1, G4 - константи 0 і 1.

G 2 = x.

і називається функцією заперечення або інверсії.

Число булевих функцій від двох змінних дорівнює . Випишемо зведену таблицю всіх цих функцій.

З виписаних функцій шість будуть виродженими, а саме функції F 1, F 4, F 6, F 11, F 13, F 16. Дійсно, легко бачити:

Решта функцій будуть невиродженим. Введемо для них спеціальні назви та позначення.

Функція F 2 носить назву кон'юнкції або твори або логічного І. Для її позначення використовується або знак множення, або Ù. Звідси:

Функція F 7 носить назву функції нерівнозначності або суми по модулю два. Для її позначення будемо використовувати:

Функція F 8 носить назву диз'юнкції або логічне АБО. Для її позначення прийнято використовувати знак Ú:

Функцію F 9 будемо називати запереченням диз'юнкції або стрілкою Пірса, і позначати через:

Функція F 10 носить назву функції рівнозначності або еквівалентності і позначається:

Функції F 12 і F 14 носять назву імплікації. Для їх позначення будемо використовувати:

Тут слід зазначити, що імплікація відповідає вислову «Якщо А, то В». При цьому виникає ситуація, що це висловлювання з помилковим А і істинним У істинно. Перш за все, це угода, причому ця угода нічому не суперечить. У повсякденній мові затвердження з помилковим А не вживаються.

Приклад типу «Якби я був космонавтом, я б полетів на Місяць» не спростовує наше твердження. Тут 1. Маємо справу не з «Якщо А, то В», а з «Якщо б А, то б В»; 2. Вважати помилковим таке твердження не має сенсу.

Виникає питання, чи можна б було при помилковому А, вважати помилковим вислів «Якщо А, то В». У принципі можна, але математична практика показує, що обраний нами варіант зручніше.

Наведемо приклад. Відомо, що при зведенні в квадрат обох частин рівняння можуть з'явитися нові корені. При цьому мається на увазі, що при зведенні в квадрат коріння загубитися не можуть. Що це означає. Це означає, що будь-який корінь рівняння:

є також коренем рівняння

Це висловлювання ми вважаємо вірним, хоча вихідне рівняння може зовсім не мати коренів. Ясно, що тут ми використовували введене угоду.

Функція F 15 носить назву заперечення кон'юнкції або штрих Шеффера. Для її позначення використовується:

Решта функції F 3 та F 5 назвемо заперечення імплікації:

Для побудови числення висловлень важливим є питання про побудову функціонально повної системи функцій.

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

Можна показати, що: Максимальне число функцій у несократімой функціонально повної системи булевих функцій від двох змінних дорівнює чотирьом. Таким чином, для булевої алгебри можна побудувати кілька варіантів функціонально повних систем. Зокрема, стрілка Пірса і штрих Шеффера кожен окремо складають функціонально повну систему. Однак найчастіше в ролі функціонально повної системи використовуються: заперечення, кон'юнкція та диз'юнкція.

Функції F 7, F 9, F 15, F 5, F 3 вже виражені через ці операції. Висловимо функції F 10, F 12, F 14.

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

Алгебраїчно перераховані вище операції можна виразити таким чином:

Заперечення (доповнення):

Кон'юнкція:

Диз'юнкція:

Тоді:

Сума по модулю 2:

Стрілка Пірса:

Еквівалентність:

Імплікація:

Штрих Шеффера:

Заперечення імплікації:

Відзначимо, що ці формули справедливі для бесконечнозначних і багатозначних логік.

Закони булевої алгебри.

Для зручності розіб'ємо закони на чотири групи.

Перша група.

1. (Закон комутативності для диз'юнкції).

2.

3. (Перший закон поглинання).

4. (Другий закон дистрибутивності).

5. (Закон Ідемпотентний для диз'юнкції).

Наступні п'ять законів виходять заміною Ù на Ú і навпаки.

1 ¢. (Закон комутативності для кон'юнкції).

2 ¢. (Закон асоціативності для кон'юнкції).

3 ¢. (Другий закон поглинання).

4 ¢. (Перший закон дистрибутивності)

5 ¢. (Закон Ідемпотентний для кон'юнкції).

Кожен із законів 1 ¢ - 5 ¢ називається двоїстим до відповідного закону 1 - 5.

Друга група

1.

2.

3.

4.

5.

6.

Третя група

1. (Закон подвійного заперечення).

2.

3.

Четверта група

1.

2. (Закон контрапозиции).

3.

Сформулюємо деякі корисні наслідки з наведених законів.

С1. Викидаючи з довільної диз'юнкції диз'юнктивні елементи рівні нулю, ми не змінимо величину цієї диз'юнкції.

С2. Якщо в диз'юнкції хоча б один з елементів дорівнює 1, то вся диз'юнкція дорівнює 1.

С3. Викидаючи з довільної кон'юнкції всі співмножники рівні 1, ми не змінимо її величини.

С4. Якщо в кон'юнкції хоча б один співмножник дорівнює 0, то весь твір дорівнює 0.

С5. Диз'юнкція чи твір будь-якого числа однакових елементів дорівнює А.

Ці слідства можна довести за індукцією.

С6. Якщо А (а1,..., Ап) довільне вираження булевої алгебри, побудоване з виразів а1,. . ., Ап за допомогою операцій заперечення, диз'юнкції і кон'юнкції, то заперечення цього виразу дорівнює , Де В (а1, ..., ап) виходить з А з допомогою заміни всіх множень на диз'юнкції, а всіх диз'юнкцій на множення, за умови збереження всіх наявних в А заперечень.

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

Нормальні форми

Елементарної диз'юнкцією називається вираз, представляє собою диз'юнкцію будь-якого кінцевого безлічі попарно різних між собою змінних, частина яких (можлива порожня) взята зі знаком заперечення. До числа елементарних диз'юнкцій будемо також відносити вираження, що складаються з однієї змінної (з запереченням або без), а також константу 0.

У силу визначення:

є елементарними диз'юнкції, а не є.

Елементарним твором називається вираз, що представляє собою твір будь-якого кінцевого безлічі попарно різних між собою змінних, над частиною яких (можливо порожній) поставлений знак заперечення. До числа елементарних творів також відносяться вирази з однією змінною з запереченням або без, а також константа 1. Елементарні твори: Неелементарному твори: Змінні і їх заперечення називаються первинними термами або літералами.

Диз'юнкція будь-якого числа первинних термів дорівнює або 1, або елементарної диз'юнкції. Твір будь-якого числа первинних термів одно або 0, або елементарного твору.

Нормальною диз'юнктивної формою (ДНФ) називається диз'юнкція будь-якого кінцевого безлічі попарно різних творів.

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

Алгоритм приведення до ДНФ і КНФ полягає в наступному.

1. Перетворити вираження згідно з операціями заперечення.

2. Використовувати перший (ДНФ) або другий (КНФ) закони дистрибутивності.

Приклад: Привести до ДНФ і КНФ вираз.

На першому етапі обробляємо знаки заперечення:

Розкриваючи дужки, приведемо до ДНФ:

При приведенні до КНФ послідовно застосовуємо другий закон до першої скобці вираження

Розглянемо деякий безліч М булевих змінних. В якості такого безлічі будемо вибирати безліч аргументів тієї чи іншої булевої функції.

Елементарні диз'юнкції називаються конституанта 0 для даної множини М булевих змінних, якщо вони містять у прямому чи інверсному вигляді всі змінні безлічі М.

Елементарні кон'юнкції називаються конституанта 1 для даної множини М булевих змінних, якщо вони містять у прямому чи інверсному вигляді всі змінні безлічі М.

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

ДНФ / КНФ називається досконалою (СДНФ / СКНФ), якщо всі складові її елементарні твору / диз'юнкції є конституанта одиниці / нуля для одного і того ж безлічі М змінних. СДНФ / СКНФ називається СДНФ / СКНФ булевої функції f, якщо вона дорівнює цієї функції і якщо безліч, складових її змінних, збігаються з безліччю аргументів функції f.

Справедливо наступне: Будь-яка булева функція має одну і тільки одну СДНФ / СКНФ.

Розглянь процес приведення до СДНФ / СКНФ.

Розглянемо довільну ДНФ j від змінних x _1,. . ., X _n. Нехай деякі елементарні твори p, що входять в цю форму, не містять будь-якої змінної x _j. Тоді ці твори можна замінити рівними їм виразами

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

Назвемо цей процес приведенням ДНФ до скоєного увазі.

Аналогічним чином можна побудувати процес приведення КНФ до скоєного увазі. Для цієї мети до входить до КНФ довільної елементарної диз'юнкції q, не містить, наприклад, змінної , Додається рівний нулю елемент . Потім до отриманого виразу застосовується другий дистрибутивний закон:

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

Приклад: Вираз привести до СДНФ і СКНФ.

1.

2.

Синтез логічних виразів.

Використовуючи таблицю істинності будь-якої логічної формули, можна визначити її в СДНФ або СКНФ. Для побудови СДНФ в таблиці істинності необхідно вибрати рядки, в яких функція приймає значення 1 та сформувати конституанту 0. Змінна буде перебувати в цій конституанті без знака заперечення, якщо вона приймає значення 1 в цьому рядку і з запереченням в іншому випадку. З'єднати отримані конституанти знаком диз'юнкції.

Для отримання СКНФ шукаються рядки, в яких функція приймає значення 0. Будуються конституанти 1. Змінна береться зі знаком заперечення, якщо вона дорівнює 1 і навпаки. Конституанти з'єднуються знаком кон'юнкції.

Приклад: Дана таблиця істинності. Побудувати СДНФ і СКНФ.

СДНФ:

СКНФ:

Мінімізація булевих функції

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

Булева функція називається импликантой функції , Якщо на будь-якому значенні змінних , На якому значення g дорівнює 1, значення f також дорівнює 1.

Простий импликантой функції f називається елементарне твір , Що є импликантой f й таке, що ніяка його власна частина (тобто твір, що отримується з g відкиданням одного або декількох компонент) вже не є импликантой функції f.

Диз'юнкція будь-якого безлічі импликант однієї і тієї ж функції є импликантой цієї функції.

Диз'юнкція всіх простих импликант булевої функції збігається з цією функцією і називається скороченою диз'юнктивної нормальною формою.

Скорочена нормальна форма є більш економною, ніж СДНФ. Однак часто допускає подальше спрощення за рахунок того, що деякі з простих импликант можуть поглинатися диз'юнкцією інших простих импликант. Наприклад, у скороченій ДНФ проста импликанта yz поглинається диз'юнкцією інших елементів форми: .

Однак справедливо наступне твердження для скороченої диз'юнктивної форми. Якщо скорочена ДНФ не містить ніякої змінної, що входить до неї одночасно з запереченням і без нього, то ця форма є мінімальною диз'юнктивної формою.

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

На перетині p-го рядка k-го стовпця импликантной таблиці ставиться * тоді і тільки тоді, коли импликанта становить деяку частину конституанти k. Для прикладу:

Система S простих импликант булевих функцій f називається наведеної, якщо ця система повна і ніяка її частина не є повною системою импликант функції f. Диз'юнкція всіх простих импликант, складових S, називається наведеної або тупикової диз'юнктивної нормальною формою. Будь-яка мінімальна ДНФ є тупиковою ДНФ.

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

Суть цього методу полягає в тому, що за импликантной таблиці будується деякий вираз, зване кон'юнктивні поданням цієї таблиці. Для цього проводиться позначення всіх простих импликант різними літерами (наприклад, A, B, C, ...). Після цього для кожного стовпця a импликантной таблиці будується диз'юнкція

всіх букв, що позначають рядки, на перетині яких зі стовпцем a варто *. Беручи твір отриманих q _a для всіх стовпців, кон'юнктивній подання таблиці. Позначимо для нашого прикладу: . Тоді отримаємо наступне подання таблиці:

Якщо у кон'юнктивній поданні розкрити всі дужки відповідно до закону дистрибутивності, отримаємо диз'юнктивні подання.

Прості імпліканти, символи яких у будь-який фіксований терм диз'юнктивного уявлення становлять повну систему простих импликант функції.

Виконуючи у диз'юнктивній поданні импликантной таблиці всі елементарні поглинання і усуваючи повторення відповідно до тотожністю АА = А і А Ú А = А, приходимо до наведеного юнктивного поданням импликантной таблиці.

Термам цього подання відповідають всі наведені системи простих импликант функції.

У прикладі отримаємо:

Тобто отримаємо 2 наведені системи простих импликант (A, B, C) ​​і (A, B, D). Їм відповідають дві тупикові ДНФ вихідної функції:

Алгоритм Квайна.

1.Мінімізіруемая булева функція f від довільного числа n змінних записується в СДНФ f _0.

2.Начіная з f _0, будуємо послідовність ДНФ f _0, f _1,. . ., F _i,. . . до тих пір поки дві будь-які ДНФ f _k і f _{k +1} не співпадуть між собою. Перехід від форми f _i до f _{i +1} за наступним правилом: у формі f _i виконуються всі операції неповного склеювання

Відповідні до елементарних творам довжини n = . Після цього виключаються всі ті елементарні твори довжини , Які можуть бути виключені на підставі формули елементарного поглинання:

.

3.Результатом алгоритму Квайна до функції f є заключна ДНФ f _k.

Для будь-якої булевої функції f результатом застосування алгоритму Квайна до СДНФ буде скорочена ДНФ цієї функції.

Приклад:

Операцію неповного склеювання можна застосувати до 1 і 3 елементу формули, до 1 і 2, а також до 1 і 4. У результаті отримаємо:

Застосовуючи формулу поглинання, отримаємо:

Оскільки операція неповного склеювання далі незастосовна, f ₁ - скорочена ДНФ.

Діаграма Вейча

Діаграми Вейча фактично являють собою іншу запис таблиць істинності і в найпростішому випадку для булевих функцій двох, трьох і чотирьох змінних мають вигляд:

Для здійснення мінімізації в таблиці необхідно виділити суміжні елементи, якими є для матриці A елементи і . Причому, операція складання виконується за модулем n, де n - розмірність матриці. Таким чином, елементи з першої і останньої рядка, з першого і останнього стовпця можуть бути суміжними. Потім вибираються групи суміжних елементів, кількість яких має бути ступенем двійки. Ці групи визначають імпліканти. Причому кількість співмножників в импликанте визначається як , Де n - число аргументів функції, - Ступінь двійки для групи елементів. При складанні імпліканти виключаються змінні, для яких одиниця є і в частині заперечення для змінної і в частині, де заперечення відсутня. Необхідно вибрати групи так, щоб їх кількість була мінімально, і всі одиниці в таблиці входили б у групи (вибираються групи з максимальним ). Отримані імпліканти зв'язуються знаком диз'юнкції.

Приклад:

Синтаксис, семантика і правила виводу в численні висловів

Синтаксис обчислення висловлювань визначається правилами граматики:

Пропозиція: = Елементарне пропозиція / Складне речення

Складне речення: = Пропозиція Зв'язка Пропозиція / ^ Пропозиція / (Пропозиція)

Зв'язка: = Ù / Ú / ^ / ® / »

Семантика обчислення висловлювань визначається за допомогою таблиць істинності.

До правил виведення відносяться:

1.

Якщо посилка А є істина, то і висновок В є істина.

2.Ісключеніе І:

Знання того, що А і В є істина, має означати, що А є істина і В є істина.

3.Інтродукція АБО:

Якщо А є істина, то А або В є істина. Те ж саме має місце, якщо В є істина.

4.Інтродукція І:

Якщо А є істина і В є істина, то А І В є істина.

5.Двойное заперечення:

Якщо А є не не істина, то А є істина.

6.Едінічная резолюція:

Якщо А або В є істина і не В, то А є істина. Точно також, якщо не А, то В - істина.

7.Резолюція:

Якщо А чи В і не В або С, то, оскільки В не може бути істинно і хибно одночасно, має бути А або З істинно.

Приклад: Є така інформація.

Якщо акумулятор машини розряджений, то машина не заводиться. Якщо машина Івана не заводиться і поточний час виявляється пізніше восьми годин ранку, то Іван запізниться на потяг. Одного разу після восьмої ранку акумулятор Івана виявився розрядженим.

Використовуючи логічні правила виводу, довести, що Іван запізниться на потяг.

У символьних позначеннях інформація може бути представлена ​​в наступному вигляді:

P: акумулятор розряджений.

Q: машина не заводиться.

R: час після восьмої ранку.

S: Іван запізнився на потяг.

Правило 1: P ® Q.

Правило 2. Q Ù R ® S.

Відомо, що P і R є істина. Завданням є довести S. Доказ будується наступним чином:

1. P - дано.

2. R - дано.

3. Q випливає з 1 і правила 1 за правилом modes ponens.

4. Q Ù R випливає з 3 і 2 за правилом інтродукції І.

5. S випливає з 4 і правила 2 за правилом modes ponens.

Обчислення предикатів передбачає, що світ можна моделювати за допомогою фактів. Але для реальних додатків обчислення висловлювань недостатньо.

Практичні завдання

Завдання 1

Дано логічні функції:

Отримати значення цих функцій за допомогою таблиць істинності. Перетворити до алгебраическому увазі і визначити значення для x = 1, y = 1, z = 0. Перетворити до виду з використанням лише операцій диз'юнкції, кон'юнкції і заперечення. Спростити. Привести до СДНФ і СКНФ. Відновити СДНФ і СКНФ за таблицею істинності. Побудувати импликантной таблицю і визначити скорочену ДНФ з використанням методу Петрика. Мінімізувати з використанням алгоритму Квайна і діаграми Вейча.

Завдання 2

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

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

Комп'ютерне завдання

Реалізувати програму вирішальну таку задачу:

На вході програми - таблиця істинності для функції чотирьох змінних.

На виході програми - СДНФ, СКНФ, діаграма Вейча і мінімальна нормальна форма.

2.2 Обчислення предикатів

Обчислення предикатів розширює мова обчислення висловлень так, що світ виявляється, що складається з об'єктів, відносин і властивостей.

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

1. Слова, що задають сутності досліджуваного світу.

2. Слова, що задають атрибути / властивості цих сутностей, а також їх поведінку і відносини.

Перший тип слів називається термами, другий - предикатами.

Деякі сутності та змінні визначаються впорядкованими послідовностями кінцевої довжини з букв і символів, виключаючи зарезервовані. Константи і змінні визначають окремі об'єкти розглянутого світу. Послідовність з n констант або змінних (1 £ n <¥), укладена в круглі дужки, наступні за символом функції, ім'я якій задане деякої кінцевої послідовністю літер, називається функцією.

Наприклад, функція f (x, y) приймає деякі значення, які визначаються значеннями констант і змінних (аргументів функції), що містяться під знаком функції. Ці значення, так само як і аргументи, є деякими сутностями розглянутого світу. Тому всі вони об'єднуються загальною назвою терм (константи, змінні, функції).

Атомарним предикатом (атомом) називається послідовність з n (1 £ n <¥) термів, укладених в круглі дужки, наступні за предикативним символом, ім'я якого виражається кінцевої послідовністю букв. Предикат приймає одне з двох значень true або false у відповідності зі значеннями, що входять до нього термів.

Предикат @ Непоширене просте речення

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

Символи першого класу дозволяють визначати новий складовою предикат, використовуючи вже певні предикати. Різниця між символами першого класу лежить в правилах, згідно з якими визначаються значення істинності або хибності складеного предиката в залежності від істинності чи хибності елементарних предикатів. Символи ® і », взагалі кажучи надлишкові так, як:

але використовуються тому ® еквівалентний фразі «Якщо А, то В», а »-« А і В еквівалентні ».

В якості символів другого класу використовуються "і $. Ці символи називаються кванторами спільності та існування, відповідно. Змінна, яка квантифікувати, тобто до неї застосований один з кванторів , Називається зв'язаною. Квантор спільності є узагальненням, аналогом кон'юнкції, а квантор існування - узагальненням, аналогом диз'юнкції на довільне, не обов'язково кінцеве безліч.

Дійсно, нехай Тоді для будь-якого предиката U виконується:

Аналогом законів Де Моргана для кванторів є:

Часто виникає ситуація, коли деякі змінні зв'язуються кванторами ", а всі інші - $. У цьому випадку може виникнути неоднозначність при інтерпретації кванторів.

Нехай задано деякий предикат U (x, y). Очевидно, що можливо вісім випадків зв'язування його кванторами існування та спільності:

Необхідно дати інтерпретацію цим восьми випадках.

Розглянемо, наприклад, предикат підсистема (x, y), який задає відношення x підсистема y. Нехай змінна x пов'язана квантором спільності, а y - квантором існування. У цьому випадку існує дві інтерпретації: 1. «Для всіх x, існує y, для яких x підсистема», 2. «Існує y, що всі x його підсистеми».

Порядок проходження пов'язаних квантором змінних визначається при читанні предиката зліва направо. Дамо інтерпретацію для інших значущих випадків, які можна виразити цим предикатом і кванторами:

• ("X) ($ y) підсистема (x, y) - всі об'єкти є підсистемами;

• ($ X) ("y) підсистема (x, y) - існує об'єкт, який є підсистемою будь-якого об'єкта;

• ("Y) ($ x) підсистема (x, y) - для будь-якого об'єкту існує об'єкт, що є його підсистемою;

• ("X) ($ y) підсистема (x, y) - існує об'єкт, який є чийсь підсистемою.

Зробимо деякі важливі узагальнення.

1.Чтоби знайти заперечення висловлювання, що починається з кванторів, треба кожен квантор замінити на його подвійний і перенести знак заперечення за квантори. Звідси:

2.Одноіменние квантори можна переставляти. Різнойменні квантори можна переставляти тільки в одну сторону. Звідси:

Якщо то

Дійсно, якщо існує об'єкт, який є чиєюсь підсистемою, то для кожного об'єкта буде існувати об'єкт, що є його підсистемою.

Якщо то

Дійсно, якщо існує y, що всі x його підсистеми, то для всіх x існує y, для якого x підсистеми. Однак, перестановка у зворотний бік невірна. Наприклад:

Якщо то необов'язково.

Дійсно, якщо для кожного об'єкта існує об'єкт, що є його підсистемою, то це не означає, що існує об'єкт, який є чиєюсь підсистемою.

3.

Доведемо цю равносильность.

У цій викладенні ми спиралися на наступне твердження:

Визначення ППФ і семантика логіки предикатів

Комбінуючи два типи символів, можна рекурсивно визначити складову формулу логіки предикатів, звану правильно побудованої формулою (ППФ) або логічною формулою.

1. Атомарний предикат є ППФ.

2. Якщо F і G є ППФ, то також ППФ.

3. Якщо F (x) - ППФ, то ("x) F (x) і ($ x) F (x) - ППФ.

4. Всі результати, отримані застосуванням кінцевого числа раз (1) - (3) є ППФ. Ніщо інше не є ППФ.

Формули логіки предикатів будуються безвідносно до понять задається предметної області. Якщо вирішено, що цими формулами буде описуватися конкретна предметна область, то має бути встановлена ​​відповідність між поняттями предметної області і цими формулами. Це передбачає наступні дії:

1. Встановлюються відповідності між константами логіки предикатів і сутностями цій галузі. Константи º Імена об'єктів.

2. Встановлюються відповідності між формулами і функціональними відносинами предметної області.

3. Встановлюються відповідності між атомарними предикатами та концептуальними відносинами предметної області.

Таким чином, у мову приноситься конкретне смислове зміст, тобто семантика логіки предикатів. Зазвичай така інтерпретація формально представляється наступним чином:

1. Задається непорожнє безліч D, що визначає сутності розглянутої предметної області, і елементи з D визначаються як константи або змінні.

2. Для функцій (функціональні відносини), визначених на множині аргументів від до D призначаються функціональні символи.

3. Кожному предикату n змінних призначається ставлення, визначене на D ^n, та її значення - True або False.

Безліч D, що розглядається з позицій логіки предикатів, називається областю змінних.

Значення ППФ оцінюються наступним чином:

1. Якщо відомі значення логічних формул F і G, то значення оцінюються за таблицею істинності.

2. Якщо для всіх x Î M F оцінюється як істина, то істиною є ("x) F (x).

3. Якщо хоча б для одного x Î M F оцінюється як істина, то ($ x) F (x) теж істина.

Пропозиції

Коли всі змінні предиката є пов'язаними, то такий предикат називається пропозицією. Різниця між ППФ, які є і які не є пропозиціями, полягає в тому, що пропозиціями можна однозначно поставити у відповідність значення True або False, в той час як у другому випадку не можна безпосередньо з вигляду формули винести судження про її істинність або хибність. Наприклад, предикатна формула підсистема (x, y) не є пропозицією. Якщо в неї підставлені певні значення, наприклад, x = процесор, y = ЕОМ, то вираз підсистема (процесор, ЕОМ) приймає значення True, а при підстановці x = людина, вираз підсистема (людина, ЕОМ) є False. Тобто істинність або хибність предикатной формули можна оцінити тоді і тільки тоді, коли в змінні підставлені деякі конкретні сутності (в цьому випадку формула називається висловлюванням). Відзначимо, що значення предикатних формул з пов'язаними змінними можна визначити, і не виробляючи такого роду підстановки.

Наприклад, - У кожної людини є батько - є істиною, а - Будь-який є чиїмось батьком - є брехнею.

Припустимо, що є деяка безліч логічних формул S. Якщо існує така інтерпретація, що всі ці формули приймають значення істина, то подібна інтерпретація називається моделлю. Наприклад, розглянемо безліч:

Тоді інтерпретація виду (людина (Сократ) = True) та (смертна (Сократ) = True) - є моделлю так як всі логічні формули S є істина. Не обов'язково, що така модель єдина.

Нехай є деяка група S логічних формул. Якщо для всіх моделей S деяка логічна формула s є істина, то прийнято говорити, що s є логічним висновком (консеквентом) в S. Факт реалізації логічного консеквента записується у вигляді S ½ = s.

Правила виводу логіки предикатів

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

У логіці предикатів в якості такого правила виводу використовується правило, яке з двох виразів A і A ® B виводить новий вираз B. Це правило називається правилом дедуктивного виводу.

Для описів правил виводу у багатьох випадках використовується нотація (як це зазначалося вище), при якій над рисою записується група виразів, які приймаються за посилку, а під рискою - вираз, який виводиться:

Такий тип правила виведення носить назву modus ponens.

Можна багаторазово використовувати одне і теж правило висновку. Наприклад, якщо крім виразів A, A ® B існує вираз B ® C, то можна вивести C, двічі використавши наведене правило. Отримання вираження s застосуванням кінцевого числа разу правила виведення до заданої групі виразів S будемо записувати у вигляді:

При цьому говорять, що s дедуктивно виводиться з S. Очевидно, що з вищевказаного, легко виводиться ще одне правило:

Практичні завдання

Завдання 1. Задано предикат виконання (x, y), який задає відношення «y є результатом виконання програми x». Дати інтерпретацію тверджень:

("X) ($ y) виконання (x, y);

($ X) ("y) виконання (x, y);

("X) (" y) виконання (x, y);

($ X) ("y) виконання (x, y);

("Y) ($ x) виконання (x, y);

($ X) ($ y) виконання (x, y).

Задано предикат реалізація (x, y), який означає «програма x реалізована на мові y». Записати твердження:

А) Існує програма, реалізована на Паскалі, має як результату 1000.

Б) Будь-яка програма, написана на C, дає результат.

3. Функціональне програмування

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

3.1 Індуктивний висновок

Індуктивний висновок - це висновок з наявних даних, що пояснює їх загального правила. Наприклад, нехай відомо, що є деяка функція від однієї змінної. Розглянемо як виводиться f (x), якщо послідовно задаються в якості даних пари значень (1, f (0)), (1, f (1)). Спочатку задається (0, 1) і має сенс запровадити постійну функцію f (x) = 1. Потім задається пари (1, 1), яка задовольняє f (x) = 1. Отже, немає необхідності міняти висновок. Нехай тепер задається (2, 3). Це не узгоджується з нашим висновком. Припустимо, що методом проб і помилок вдається знайти . Вона задовольняє заданим досі фактам. Далі, якщо будуть слідувати факти (3, 7), (4, 13), (5, 21), ..., переконаємося в справедливості попереднього висновку. Таким чином в індуктивному виведення в кожен момент часу пояснюються всі дані, отримані до цього моменту. Якщо дані, пізніше, перестануть задовольняти отриманому висновку, то його доведеться міняти. Отже, індуктивний висновок - це необмежено довгий процес.

Для визначення індуктивного виведення необхідно уточнити:

1. Безліч правил об'єктів виводу.

2. Метод подання правил.

3. Спосіб показу прикладів.

4. Метод виведення.

5. Критерій правильності висновку.

В якості правил - об'єктів висновку можна розглядати:

• функції;

• граматики мов;

• програми.

Метод подання зручно організовувати у вигляді пар (x, f (x)), послідовності дій, який обчислює f (x) і т.д.

Висновок реалізується завдяки необмеженому повторення процесу:

Запит вхідних даних ® припущення ® вихідні дані.

Критерієм правильності висновку вважається ідентифікація в межі. Кажуть, що машина виведення M ідентифікує в межі правило R, якщо при показі прикладів правилом R послідовність вихідних даних, що генеруються M, збігається до деякого поданням t, а саме: усі вихідні дані, починаючи з деякого моменту часу, збігаються з t, при цьому t називають правильним поданням R. Крім того, говорять, що безліч правил G дозволяє зробити індуктивний висновок, якщо існує деяка машина виведення M, яка ідентифікує в межі будь-яке правило R з безлічі G.

Характерним прикладом індуктивного висновку є математична індукція.

3.1.1 Математична індукція

Методом математичної індукції називаються затвердження види:

Нехай змінна n має область N (натуральні числа). Щоб довести перше твердження, достатньо довести два твердження:

(4)

(5)

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

U (k) ® U (k +1) (6)

Як випливає з визначення квантора спільності, довівши це отримаємо (5). Для доказу (6) припускають, що істинна посилка:

U (k) (7)

і виводять з цього припущення, що правдиве її висновок U (k +1). Затвердження (7) називається припущенням індукції.

При доведенні затвердження (2) базисом індукції є твердження U (a), індукційним кроком - ("n ³ a) (U (n) ® U (n +1)), припущенням індукції - затвердження U (k), де k - довільне натуральне число більше або рівне a.

При доведенні твердження (3) базисом індукції є твердження U (a), індукційним кроком - затвердження ("n: a £ n <b) (U (n) ® U (n +1)), припущенням індукції U (k), де k - довільне натуральне число таке, що a £ n <b. Така індукція називається індукцією по інтервалу. Від індукції по інтервалу можна перейти до індукції спуску. Індукцією спуску називається індукція, базисом якої є твердження U (b), індукційним кроком - затвердження ("n: a £ n <b) (U (n +1) ® U (n)). Передумовою індукції в цій формі є твердження U (k +1), де k - довільне натуральне число таке, що a £ n <b.

Іноді твердження 1 зручно доводити поворотної індукцією. Поворотна індукція - це індукція з базисом U (1), але з індукційним кроком ("n) (" m £ n) (U (m) ® U (n)). Передумовою індукції є ("m <k) U (m), де k - довільне натуральне число. Поворотна індукція зі зміненим базисом і індукційним кроком застосовується і при доказі тверджень 2 і 3.

Для доведення тверджень 1-3 часто буває зручною індукція з подвійним базисом, тобто для випадку 1 індукція з базисом U (1) Ù U (2) і індукційним кроком ("n) ((U (n) Ù U (n +1 )) ® U (n +2)). Іноді зручно застосовувати індукцію з потрійним, чотириразовим і т.д. базисом.

Для доведення тверджень виду

(8)

застосовується індукція за двома змінним. Однак, твердження (8) часто вдається звести до індукції по одній змінної. Для цього формуємо в якості значення змінної m довільне число і позначаємо його а. Доведемо твердження ("n) U (a, n). З цього твердження, очевидно, слід (8). Але останнє твердження має вигляд 1 і його можна довести індукцією. При такій схемі n називається індукційної змінної. Кажуть також, що (8) доводиться по n при фіксованому m.

3.1.1 Практичні завдання

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

Нехай A змінна з областю визначення R (N) (множини натуральних чисел), n - Змінна з областю визначення N (натуральні числа). Позначимо через U (A, n) вислів: «Якщо множина A містить n елементів, то в A немає двох нерівних натуральних чисел ». Очевидно, твердження

рівносильно утвердженню завдання.

Доведемо твердження (1) індукцією по n, причому індукцію будемо застосовувати у її найпростішій формі. Базисом індукції є:

("A) U (A, 1). (2)

Доведемо (2). Візьмемо довільне M Ì N і доведемо

U (M, 1). (3)

Тим самим буде доведено твердження (2). Але на основі визначення U, (3) стверджує: «Якщо множина M містить один елемент, то в M немає двох нерівних натуральних чисел», що очевидно. Припустимо тепер як припущення індукції, що ("A) U (A, n) вірно для деякого натурального k, тобто, що вірно

("A) U (A, k) (4)

і доведемо, що вірно

("A) U (A, k +1) (5)

Тим самим твердження (1) буде доведено. Для доказу (5) візьмемо довільне M Í N і доведемо

U (M, k +1) (6)

Тим самим (5) буде доведено. На основі визначення U, (6) є твердження: «Якщо множина M містить k +1 елементів, то в M немає двох нерівних натуральних чисел ». Щоб довести цю імплікації, припустимо, що її посилка вірна. Пронумеруємо як-небудь елементи множини M. Нехай, наприклад:

Доведемо, що в множині M немає двох нерівних натуральних чисел. Тим самим доказ буде закінчено. Розглянемо два допоміжних множини:

Кожне з них отримано викиданням з M одного елемента і, отже, містить k елементів. У силу припущення індукції (4) U (K, k) - «Якщо безліч K містить k елементів, то в K немає двох нерівних натуральних чисел». Але безліч K якраз містить k елементів, отже, в ньому немає двох нерівних натуральних чисел. Звідси:

(7)

Використовуємо ще раз припущення індукції (4). Візьмемо тепер як значення A безліч L. Тепер з (4) отримаємо твердження U (L, k), що означає: «Якщо безліч L містить k елементів, то в ньому немає двох нерівних натуральних чисел». Але безліч L містить саме k елементів, отже, в ньому немає двох нерівних натуральних чисел. Зокрема:

(8)

З (7) і (8) випливає, що в M немає двох нерівних натуральних чисел. Доказ закінчено.

3.2 Рекурсія

Особливе місце для систем функціонального програмування набуває рекурсія, оскільки вона дозволяє враховувати значення функції на попередніх кроках.

З теоретичної точки зору рекурсивні означення є теоретичною основою всієї сучасної теорії вичіслімих функцій. Розглянемо два способи обчислення f (1) + f (2) + ... + f (n). При ітерації зробимо таким чином. Визначимо підпрограму:

Sub Add (S, k, f)

S = S + f

k = k -1

End Sub

Тоді процедуру без використання циклу можна визначити наступним чином:

S = 0

k = n

I: Add (S, k, f (k))

J: If k ¹ 0 Then Goto I

Тут підпрограма Add виконується n разів послідовно і незалежно, причому кожен раз використовується тільки одна команда повернення. Це ітерація.

Для рекурсії побудуємо функцію:

If k = 0 Then

Sum (f, k) = 0

Else

Sum (f, k) = f (k) + Sum (f, k-1)

End If

Тепер достатньо просто дізнатися значення Sum (f, n). Розглянемо окремий випадок при n = 2. З визначення випливає, що необхідно обчислити f (2), а потім звернутися до обчислення Sum (f, 1), результат обчислення якого повинен бути доданий до f (2). Отже, зберегти в пам'яті f (2), встановити ще один повернення і звернутися ще один раз до нашого визначенням. Тепер обчислюємо f (1), знову запам'ятовуємо результат у пам'яті, встановлюємо третє повернення і в третій раз звертаємося до визначення для обчислення Sum (f, 0). Остання функція дорівнює 0, і ми виходимо з визначення, використовуючи повернення, встановлений перед зверненням до визначення. Далі додаємо 0 до f (1), знову виходимо з визначення, використовуючи другий повернення, додаємо 0 + f (1) до f (2) і виробляємо остаточний вихід. Це рекурсія. Визначення Sum використовувалося не послідовно і незалежно, а з вкладенням подальшого використання в попереднє (що характерно для індуктивного виводу), три команди повернення одночасно зберігалися в пам'яті і використовувались за принципом «останній прийшов - виконався перший» (LIFO).

Тут ми розглянули приклад простої рекурсії. Іншим більш складним прикладом рекурсії є обчислення чисел Фібоначчі. Їх можна визначити за допомогою таких формул:

Формально число Фібоначчі можна обчислити за такою явною формулою:

F (n) = [(1 + Ö 5) ⁿ - (1 - Ö 5) ^n] / (2 ⁿ Ö 5).

Ця формула відносно складна. Насправді в цьому виді завдання навіть повністю не вирішена, оскільки алгоритм використання формули потрібно уточнити. Наприклад, чи здійснювати розкриття внутрішніх дужок за формулою бінома? Яке значення брати для числа Ö 5, тобто скільки брати десяткових знаків? Очевидно, що хоча результат повинен бути цілим, він не буде таким. Отже, постає питання, до якої сусідньої цілого потрібно округляти? Як бути при цьому впевненим у результаті?

Для цієї мети можна використовувати рішення з безпосередньою підстановкою:

Sub F (n)

If n> 2 Then

F (n) = F (n - 1) + F (n - 2)

Else

F (n) = 1

End If

End Sub

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

A (m, n) = iif (m = 0, n +1, iif (n = 0, A (m-1, 1), A (m-1, A (m, n-1 )))).

Взагалі кажучи, обчислення таких функцій може бути нескінченним (характерна особливість індуктивного виводу). Як приклад наведемо функцію f (m, n), результатом якої є 1 у випадку, якщо в десятковому запису числа p зустрічається фрагмент з послідовності цифр, що повторюються m довжиною n.

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

У залежності від того, як оформлений виклик рекурсії, можна виділити ще кілька її різновидів. Рекурсія називається паралельної, якщо вона зустрічається одночасно в декількох аргументах функції, тобто коли тіло визначення функції f, містить виклик деякої функції g, кілька аргументів якої є рекурсивним викликом f:

f (... g (..., f, ..., f, ...)).

Рекурсія є взаємною між двома або більше функціями, якщо вони викликають один одного, тобто коли у визначенні функції f викликається функція g, яка у свою чергу містить виклик функції g:

f ((...) (... g ...));

g ((...) (... f ...)).

Рекурсія більш високого порядку є рекурсією, в якій аргументом рекурсивного виклику є рекурсивний виклик:

f (... f (... f ...) ...).

3.2.1 Комп'ютерне завдання

Дана послідовність символів a 1, a 2, ..., an. Із застосуванням рекурсії реалізувати процедуру інверсії даної послідовності, тобто процедуру отримання послідовності b 1, b 2, ..., bn такий, що b 1 = an, b 2 = an -1, ..., bn -1 = a 2, bn = a 1.

3.3 l-числення

В алгебрі наводиться чітке розходження між пов'язаними і вільними змінними в контексті деяких конструкцій. Усередині цих конструкцій вільні змінні мають той же зміст, що і поза ними. Зв'язані ж змінні повністю належать самим конструкціям і поза них порожні, тобто можуть бути замінені будь-якими літерами (за винятком тих, які використовуються в даній конструкції).

У вираженні

буква x може бути замінена будь-який інший буквою (за винятком t або f) і сенс висловлювання від цього не зміниться в будь-якому контексті, де цей вираз може бути використано.

У визначенні функції виду:

... Де g (x) = a sin (px + q)

буква x також порожня.

З точки зору обчислювальної математики виникає проблема, чи є x ім'ям об'єкта (областю робочої пам'яті) чи ні; або x - Це об'єкт, значенням якого є інше ім'я. Цей варіант може мати подальший розвиток, коли фактичний параметр у g (x) є вираженням відмінним від простої змінної, наприклад, як у записі g (t ² + 2).

Очевидно, що в основі лежить питання визначення функцій. Для цих цілей у 1941 році Черчем було введено l-числення. Поставити функцію - це означає вказати закон відповідності, що приписує значення функції кожному допустимого значення аргументу. Нехай M - Деяка формула, що містить x в якості вільної змінної. Тоді l x. [M] є функція, значення якої для будь-якого аргументу виходить підстановкою цього аргументу в M замість x. Операцію освіти вираження l x. [M] з M і x називають l - операцією або функціональної абстракцією.

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

Основним поняттям є поняття функції f, яка зіставляє принаймні один об'єкт f (x _1, ..., x _n) (її значення) з кожного n - кою об'єктів x _1, ..., x _n (її аргументів, які самі можуть розглядатися як функції). l - обчислення дозволяє враховувати специфіку обчислення функції залежно від використовуваних аргументів, тобто від того який з аргументів розглядається як пов'язана змінна.

Наприклад, у диференційному численні вираз x - y може розглядатися як функція f від x, або як функція g від y. Для того, щоб їх розрізняти будемо записувати:

f = l x. [xy], g = l y. [xy].

Кажуть, що префікс l x абстрагує функцію l x. [x - y] від виразу x - y.

Аналогічні позначення застосовуються для функцій від багатьох змінних. Наприклад, x - y відповідає функціям від двох змінних h і k: h (x, y) = x - y, k (y, x) = - y + x. Це можна записати:

h = l xy. [xy], k = l yx. [xy].

Однак, можна уникнути використання функцій від декількох змінних, якщо використовувати функції, значеннями яких є функції.

Наприклад, визначимо функцію:

s = l x. [l y. [x - y]],

яка для кожного числа a перетворюється на

s (a) = l x. [l y. [xy]] (a) = l y. [ay],

а для кожної пари a, b в

s (a (b)) = s (a, b) = l x. [l y. [xy]] (a, b) = ab.

Припустимо, що є нескінченна послідовність змінних і кінцева або нескінченна послідовність констант. Атом визначається як змінна або константа. Безліч l - термів визначається індуктивно:

1. Кожен атом є l - терм.

2. Якщо X і Y - l - терми, то (XY) - l - терм.

3. Якщо Y - L - терм, а x - змінна, то l x. [Y] - l - терм.

Наведене вище визначення функції g (x) в цьому обчисленні записується таким чином:

g = l (x). [a * sin (p ​​* x + q)],

а замість g (t ² + 2) можна записати:

l (x). [a * sin (p ​​* x + q)] (t ² + 2).

За символом l слід ще декілька синтаксичних конструкцій: спочатку йде список пов'язаних змінних, потім вираз, до якого входять ці змінні (тіло l - вираження). Якщо зупинитися тут, то будемо мати функцію без операндів, таку як sin (заголовок функції). Але далі може слідувати список фактичних операндів. У цьому випадку маємо результат: взяття функції від цих операндів.

Важливе значення набуває поєднання l - обчислення і рекурсії. Припустимо, що існує функція «слідуючий» - назвемо її next (x) - для кожного цілого додатного числа і нуля. Насправді - це функція x + 1, але будемо вважати, що + поки не визначений.

Використовуючи next, можемо задати функцію «попередній» - prior (x) (після визначення - ця функція буде мати вигляд x -1). Визначимо цю функцію наступним чином:

prior (x) = previous (x, 0) Where previous (y, z) = iif (next (z) = y, z, previous (y, next (z))).

Процес обчислення prior (x) розпочинається за z = 0, далі послідовно обчислюються послідовно функції next до тих пір, поки наступний для z не буде дорівнює x. Це значення z і є відповіддю. Тепер можемо визначити суму та різницю двох чисел.

Sum (x, y) = iif (y = 0, x, Sum (next (x), prior (y))),

Diff (x, y) = iif (y = 0, x, Diff (prior (x), prior (y))).

Звернемо увагу, що якщо y> x, то при обчисленні Diff настане такий момент, коли буде потрібно обчислення prior (0), а серед позитивних чисел немає попередника нуля. Тому кажуть, що Diff обчислюваною тільки частково для позитивних чисел.

Тепер уявімо Sum в l - обчисленні:

Sum = l (x, y). [Iif (y = 0, x, Sum (next (x), prior (y)))]

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

Sum = l f. L (x, y). [Iif (y = 0, x, Sum (next (x), prior (y )))]( Sum),

а потім можна зовсім прибрати об'єкт визначення з правої частини за рахунок введення оператора Y такого, що якщо F - функція, то Y F - рішення рівняння y = F (x).

Sum = Y l f. L (x, y). [Iif (y = 0, x, f (next (x), prior (y )))].

У цьому визначенні f - Пов'язана змінна, яка при дозволі рівняння може бути замінена на що-небудь інше. Отже, при заміні на Sum отримаємо:

Sum = Y l Sum. L (x, y). [Iif (y = 0, x,. Sum (next (x), prior (y )))].

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

Кажуть, що l - обчислення використовується для того, щоб виконати операцію l - редукції і спростити вираз.

Враховуючи, що вираз l x. [Px] (a) може бути зредуковано до Pa, вираз:

l f. l y. l x. [f (x, y)],

сформульоване:

l f. l y. l x. [f (x, y)] (підсистема)

зводиться до

l y. l x. [підсистема (x, y)],

l y. l x. [підсистема (x, y)] (ЕОМ) ® l x. [підсистема (x, ЕОМ)], а

l x. [підсистема (x, ЕОМ)] (процесор) ® підсистема (процесор, ЕОМ).

Таким чином, l - редукція здійснюється зліва направо, і тому l f. L y. L x. [F (x, y)], сформульоване у вигляді l f. L y. L x. [F (x, y)] (любить, Марія, Іван), дає любить (Іван, Марія).

3.3.1 Практичні завдання

1.Визначити функцію f (x, y) = iif (x> y, sin (x), cos (x)) в l - численні. Дати її запис для x = t і y = p / 2. Здійснити редукцію.

2.Осуществіть редукцію наступних l - виразів:

l f. [l g. [l t. [f (g (x) + t (y )]]]( sin, cos, tg),

l g. [l t. [l f. [f (g (x) + t (y )]]]( sin, cos, tg),

l f. [l t. [l g. [f (g (x) + t (y )]]]( sin, cos, tg),

3.4 Використання списків

Введемо деякі визначення. Символ - це набір літер, цифр і спеціальних знаків. Крім символів будемо використовувати: числа, Т - істина, Nil - брехня або порожній список. Будемо розуміти під константами - числа, Т, Nil. Будемо розуміти під атомами символи та числа. Назвемо списком упорядковану послідовність, елементами якої є атоми або інші списки (підсписки). Будемо укладати списки в круглі дужки, а елементи списку розділяти пробілами.

Формально список можна визначити наступним чином:

Список: - Nil / (голова Ç хвіст)

[Список або порожній, або це пара голова і хвіст]

голова: - атом / список

[Рекурсія в глибину]

хвіст: - список

[Рекурсія в ширину]

Інший варіант визначення:

Список: - Nil / (елемент елемент ...)

Елемент: - атом / список

[Рекурсія]

Звернемо увагу, що атом це не список, хоча символ може ідентифікувати список. Кожен символ має значення. Ним може бути список, в тому числі і порожній, константа, функція, яку розглядають як спеціальний символ. Для запису функцій будемо використовувати префіксной нотацію, тобто x + y будемо записувати, як (+ x y).

Атоми і списки будемо називати S - виразами.

Для подання списків будемо використовувати сукупність комірок пам'яті, кожна з яких містить два покажчика. Перший покажчик грає роль покажчика на сина, другий - на брата. Наприклад, список (А В) буде мати вигляд.

Відсутність покажчика будемо позначати символом y.

Список (* (+ 2 3) с) буде мати уявлення:

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

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

Цією схемою відповідає список ((А) (В)).

Повернемося до визначення атома. Фактично атоми є функціями, аргументи яких є наступні за ними S - вирази. У свою чергу аргумент сам може бути функцією, яку треба знайти. Тому виникає необхідність визначати, що є даний елемент: значення виразу L або символьне ім'я L якогось S - вирази. У першому випадку перед вираженням ставиться 'або покажчик QUOTE. Апостроф забороняє обчислення наступного за ним S - висловлювання, яке відтворюється без змін.

Для завдання виразів введемо функцію Setq:

(Setq <атом> <S - вираз>)

(Setq <атом> '<S - вираз>)

У першому випадку вираз повинен бути обчислено, у другому - на обчислюється. Крім того, Setq пов'язує отриманий результат з атомом.

(Setq L1 (+ 4 5))

(Setq L1 '(+ 4 5))

У першому випадку L 1 пов'язано з (9), у другому - з (+ 4 5).

Функція CAR повертає як значення перший елемент списку, тобто його голову. Функція має сенс, тільки для аргументів, що є списками, мають голову.

(CAR '(ABC)) ® A

(CAR 'A) ® помилка, А не список.

Функція CDR повертає хвіст списку. Якщо список складається з одного елемента, то результатом є Nil.

(CDR '(ABC)) ® (BC)

Комбінація викликів CAR і CDR виділяє довільний елемент списку. Для простоти цю комбінацію записують у вигляді:

(C ... R список)

Замість трьох крапок записується комбінація з букв А (для CAR) і D (для CDR).

(CADDAR L) = (CAR (CDR (CDR (CAR L))))

Функція CONS будує новий список із переданих йому голови і хвоста.

(CONS голова хвіст)

(CONS 'a' (bc)) ® (abc)

(CONS '(ab)' (cd)) ® ((ab) cd)

(CONS (+ 1 2) '(+ 4)) ® (3 + 4)

Тут перший аргумент без апострофа, тому береться як значення.

(CONS '(+ 1 2)' (+ 4)) ® ((+ 1 2) + 4)

(CONS '(abc) Nil) ® ((abc))

(CONS Nil '(abc)) ® (Nil abc)

Предикат ATOM використовується для аналізу списків, а саме, для ідентифікації чи є об'єкт атомом чи ні.

(ATOM 'x) ® T

(ATOM (CDR '(ABC))) ® Nil. Атом від списку (B C) природно False.

(ATOM (ATOM (+ 2 3))) ® T.

Результат додавання чисел атом. Т також є атомом.

(EQUAL <S-вир1> <S-вир2>) ® T, якщо і тільки якщо значення обох виразів рівні.

(EQ <S-вир1> <S-вир2>) ® T, якщо і тільки якщо значення обох виразів рівні і представляють один фізичний список.

(AND <S- вир 1> <S- вир 2> ... <S-вир n>) - якщо зустрічається Nil,, повертається Nil, інакше значення останнього виразу.

(OR <S- вир 1> ... <S-вир n>) - якщо при перегляді зустрічається вираз відмінне від Nil, то вона повертається, інакше Nil.

(NOT <S-вир>) ® T, якщо і тільки якщо значення виразу є Nil.

Визначати функції будемо згідно l - обчисленню.

(L (x _1, x _2, ..., x _n) f)

x _i - формальний параметр.

f - тіло функції.

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

(L (xy) (+ (* xx) (* yy))).

Щоб зробити обчислення будемо здійснювати l - виклик.

(L - вираз a _1, ..., a _n),

Тут a _i - форма, що задає фактичні параметри.

((L (x y) (+ (* x x) (* y y))) 2 3) - дає 13.

Для того щоб визначити нову функцію будемо використовувати запис:

(DEFUN <ім'я> <l - вираз>).

Для зручності виключимо значок l і зовнішні дужки.

(DEFUN відсотки (частина ціле) (* (/ частина ціле) 100)).

Виклик:

(Відсотки квітня 1920)

Результат: 20.

Умовний вираз COND має наступний вигляд:

(COND (p1 a1)

(P2 a2)

. . .

(Pn an))

Значення COND визначається наступним чином:

1. Вирази pi обчислюються послідовно зліва направо (зверху вниз) до тих пір, поки не зустрінеться вираз, значення якого відмінно від Nil.

2. Обчислюється результуюче вираз ai відповідне цьому pi і отримане значення повертається в якості результату.

3. Якщо немає ні одного pi, значення якого відмінно від Nil, то значення COND одно Nil /

У більш загальному вигляді:

(COND (p1 a1)

...

(Pj)

...

(Pk ak ₁ ... ak _n)

...)

У цьому випадку:

• якщо умові не ставиться у відповідність результуюче вираз, то в якості результату при істинності предиката видається саме значення предиката;

• якщо умові відповідає кілька S - виразів, то при його істинності вони обчислюються зліва направо і результатом буде значення останнього S - вирази.

Реалізуємо логічні зв'язки І, АБО, ®.

(Defun І (xy) (COND (xy) (T Nil)))

(Defun АБО (xy) (COND (x T) (T y)))

(Defun ® (xy) (COND (xy) (TT)))

За допомогою COND можна реалізувати різні варіанти умовних виразів.

(If <умова> <те-вир> <інакше-вир>) º (COND (<умова> <те-вир>) (T <інакше-вир>))

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

(PUTPROP <атом1> <список> <атом2>).

Ця функція пов'язує властивості, виражені списком <атом2>, з конкретним об'єктом з ім'ям <атом1>. Конкретні значення властивості задаються в об'єкті <список>.

(PUTPROP 'Петро' (Іван Ірина) 'Діти).

Щоб дізнатися чи має об'єкт даними властивістю, будемо використовувати функцію GET:

(GET <атом1> <атом2>) ® значення властивості.

(GET 'Петро' Діти) ® (Іван Ірина)

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

Цей алгоритм представимо в виду процедури Eval (S), де S - вираз.

Sub Eval (S)

If S є атом then

Повернення ¬ значення S

Else

If S1 = QUOTE then

Повернення ¬ S 2

Else

S 1 є функція

If S 1 вказує на спеціальну обробку, виконати цю обробку

Else

Застосувати Eval до всіх елементів S 2 послідовно і потім рекуррентно використовувати їх знайдені значення.

Остаточний повернення ¬ S 1 (Eval (S 2))

End If

End If

End If

S 1 - перший син для S. S 2 - елементи вираження S, що представляють собою безліч братів вираження S 1.

3.4.1 Практичні завдання

1.Создать машинне подання для списків:

(A (bc) ((d) e (f)))

(+ A (* b (/ (+ c (/ de)) f)))

(/ (+ (A (- (bc)))) (* (/ (db)) a))

(Flat (hd (a) flat (tl (a) b)))

(Cons (copy (hd (l))) copy (tl (l )))))

2.Визначити значення списків:

(Car '(a (bc) ((d) e (f))))

(Cdr '(a (bc) ((d) e (f))))

(Cdadr '(a (bc) ((d) e (f))))

(Cons nil '(суть порожній список))

(Cons (car '(ab)) (cdr' (ab)))

(Car '(car (abc)))

(Cdr (car (cdr '(abc))))

3.Запішіте послідовність викликів CAR і CDR, що виділяли б із наведених списків символ «мета». Спростіть ці послідовності за допомогою функцій C ... R.

(1 2 мета 3 4)

((1) (2 мета) (3 4 мета)))

((1 (2 (3 4 мета))))

4.Визначите вид списку, що має наступне машинне подання:

4. Реалізувати з допомогою COND логічні операції: еквівалентність, штрих Шеффера, стрілка Пірса.

5. Реалізувати функцію reverse, переставляти місцями елементи списку.

3.4.2 Комп'ютерне завдання

Створити БД для індуктивного виводу та реалізувати програму заповнення цієї бази для оператора Setq. Можлива структура таблиці для зберігання списків:

Приклад заповнення:

Нехай послідовно створюються 2 списку:

Setq a (* (+ 2 3) c)

Setq Second ((a) (b))

Структура списків: Список а

Список Second

Таблиця для цих списків буде мати вигляд:

Порядок виконання

1. Створення таблиць і форм для введення і зберігання списків (1 заняття).

2. Реалізація алгоритмів перетворення опису списку в машинне подання і назад (2 заняття).

3. Реалізація операцій над списками (2 заняття)

4. Реалізація алгоритму Eval (2 заняття).

5. Оформлення результатів (1 заняття).

4. Логічне програмування

Логічне програмування базується на уявленні завдань у вигляді теорем, доказуваних в рамках обчислення предикатів першого порядку.

4.1 Моделі і спростування

У доказі теорем намагаються показати, що певна ППФ B є логічний наслідок безлічі ППП S = {A _1, ..., A _n}, званих аксіомами розглянутої задачі. Правило висновок є правило, за допомогою якого з раніше отриманих виразів можна отримати нове. Наприклад, якщо A _i і A _j істинні ППФ, то запис:

вказує, що A _k можна отримати з A _i і A _j за допомогою правила f _q . Розглянемо послідовність S (0), ..., S (j +1), утворену з деякого безлічі аксіом S за правилом:

S (0) = S,

...

S (j +1) = S (j) È F (S (j),

де F (S) - безліч виразів, яку можна отримати з безлічі S, застосовуючи до кожного його елементу всі можливі правила f _q з кінцевого безлічі F = {f _q}. Кажуть, що висловлювання B випливає з аксіом, що належать S, якщо B Î S (j) для деякого j.

Нагадаємо, що терм - це константа, змінна або функція. В якості своїх аргументів n - місцева функція повинна мати п термів. Таким чином, термами будуть: a, b, c, f (a), g (f (x), y).

Атомом називається предикат зі своїми аргументами. Літерал - це атом або його заперечення. Пропозиція C - це диз'юнкція літералів. Безліч пропозицій S інтерпретується як єдине висловлювання, що представляє кон'юнкцію всіх його пропозицій.

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

Для того, щоб висловлювання S È T були істинними, всі пропозиції C _i і T повинні бути істинними. У свою чергу значення істинності цих пропозицій будуть визначатися значеннями істинності, що містяться в них атомів, причому значення істинності повинні присвоюватися атомам так, щоб, принаймні, один літерал в кожному реченні був істинним.

Окрему присвоювання істинності атомів називається моделлю. Якщо S тягне за собою T, то не існує моделі, в якій S істинне, а T - Ні. Разом з тим, якщо висловлювання T істинне, то його заперечення повинно бути помилковим. Тому, якщо S тягне за собою T, вислів:

(1)

повинно бути помилковим для будь-якої моделі.

Цей же висновок можна зробити наступним чином:

і від протилежного:

Припустимо, що число атомів звичайно. Тоді існує кінцеве безліч моделей, так як k атомам можна привласнити логічні значення 2 ^k різними способами. Очевидно, що присвоювати значення цим комбінаціям можна послідовно і якщо для всіх моделей (1) виявиться помилковим, то, безумовно, S тягне T. Такий доказ називається методом від протилежного і складає основу методів доведення теорем.

Довести суперечливість (1), якщо число атомів звичайно, досить просто. Чи то просто на практиці залежить від кількості атомів і від можливості породжувати і перевіряти моделі.

Виникає задача виявлення умов, що гарантують кінцеве число атомів. Нехай S - Це безліч висловлювань істинних для тих атомів, які безпосередньо входять в S і тих, які з них можна вивести. Остання множина може бути нескінченним. У цьому можна переконатися на такому прикладі. Нехай S - Вислів, що містить єдиний атом S = {R (a, x)}.

Припустимо, що визначена функція g (x). Тоді можемо побудувати нескінченну послідовність R (a, x), R (a, g (x)), R (a, g (g (x))), .... Ця послідовність перераховувані, тому що можна придумати схему перерахування, за якою впорядковуються висловлювання. Наприклад, за рівнем вкладеності другого аргументу. Можна показати, що завжди можна побудувати схему перерахування нескінченної кількості атомів, отриманого з кінцевого за допомогою деякої підстановки.

Припустимо, що S не містить змінних. Така ситуація називається основним випадком, а відповідний універсум (область визначення) Ербрановой базою. В основному випадку можна провести перерахування.

Доведемо, наприклад, для конкретної пари чисел (a, b) (але не для довільної пари чисел взагалі x, y) істинність вислову:

a = b ® a> b.

Аксіомами будуть:

A1: a> b,

A2: a <b,

A3: a = b.

Відповідні пропозиції будуть мати вигляд:

- Виконується одна з відносин;

- Одночасно не виконуються ніякі два відносини.

У цих позначеннях наше твердження має вигляд:

і його заперечення A 3 A 1. Звідси отримаємо:

Позначимо

Так як в S може бути тільки 2 ³ = 8 атомарних висловлювань, легко побудувати всі можливі моделі. Якщо для кожної з них хоча б одне речення в S приймає значення брехня, то висловлювання виду (1) буде хибним, і тому наше твердження буде істинним.

Цей метод неефективний і надмірний. Можна показати, що висловлювання S суперечливо, якщо дослідити менше число моделей. Досить обмежитися атомами A 1 і A 3, тобто провести привласнення значень істинності тільки цим атомам, а значить, використовувати тільки чотири моделі.

Теорема Ербрана - Сколема - Геделя. У цій теоремі стверджується, що можна знайти часткове присвоювання, приписують значення брехня будь суперечливого безлічі пропозицій.

4.2 Доведення від супротивного

4.2.1 Неаксіоматіческое опис процедури

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

Нехай в якості å задана група логічних формул такого вигляду:

Батько (x, y): x є батьком y;

Брат (x, y): x, y - брати;

Кузен (x, y): x, y - двоюрідні брати;

Дідусь (x, y): x - дідусь y.

Використовуючи ці предикати можна записати наступні твердження:

(1) ("x 1) (" y 1) ("z 1) ((батько (x 1, y 1) Ù батько (y 1, z 1)) ® дідусь (x 1, z 1)):

якщо x 1 батько y 1, а y 1 батько z 1, то x 1 дідусь z 1.

(2) ("x 2, y 2, z 2, w 2) ((батько (x 2, y 2) Ù брат (x 2, z 2) Ù батько (z 2, w 2)) ® кузен (y 2, w 2)).

(3) ("x 3, y 3, z 3) ((батько (x 3, y 3) Ù батько (x 3, z 3) Ù ) ® брат (y 3, z 3)).

Припустимо також, що крім цих логічних формул задані наступні факти:

(4) Батько (Олександр, Сергій),

(5) Батько (Сергій, Річард).

(6) Батько (Сергій, Іван).

Спочатку неаксіоматіческі задамо процедуру, яка з логічних формул виводить висновок. Виведення формули C з логічних формул A, B будемо задавати у вигляді схеми:

А: Всі люди смертні

В: Сократ - людина

З: Сократ - смертна.

Якщо в змінну підставляється значення, то зліва від похилої риси запишемо ім'я змінної, а праворуч - значення. Наприклад, якщо в змінну x підставляється значення Сократ, то будемо це записувати як x / Сократ.

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

Наприклад, припустимо, що поставили запитання: «Хто дідусь Річарда?». Його можна записати у вигляді:

($ X) (дідусь (x, Річарда)).

Відповідь може бути отриманий в такій послідовності:

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

З іншого боку можна здійснити і спадний висновок. Спадний висновок починається з того висновку, який повинен бути одержаний, і далі в базі проводиться пошук інформації, яка послідовно дозволяє прийти до даного висновку.

У логіці предикатів така процедура повністю формалізована і носить назву методу резолюції.

Для застосування цього методу вихідну групу логічних формул перетворять в нормальну форму. Перетворення проводиться у кілька стадій.

4.2.2 Процес нормалізації

4.2.2.1Префіксная нормальна форма

Розглянемо фразу «будь-яка людина має батька». Її можна представити у логіці предикатів у наступному вигляді:

("X) (осіб (x) ® ($ y) (батько (y, x))).

$ Знаходиться всередині ППФ. Це не завжди зручно, тому доцільно винести всі квантори за дужки, щоб вони стояли перед ППФ. Така форма має назву префіксной нормальної форми.

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

По-перше, необхідно виключити зв'язки ® і ». За визначенням:

Отже, у всіх комбінаціях ППФ можна обмежитися трьома зв'язками Ú, Ù і `.

Предикат, що не містить змінних, аналогічний висловом, тому такі предикати будемо позначати F, G. Коли деякий вираз виконується для будь-якого квантора "і $ будемо записувати такий квантор Q.

Легко показати:

1.

Це відповідає: вислів не має відношення до квантор змінної, яка включена в іншій предикат.

Між предикатами існує наступне співвідношення:

Таким чином, «необов'язково F (x) виконується для всіх x» º «існує таке x, що F (x) не виконується», «не існує таке x, що виконується F (x)» º «для всіх x не виконується F (x) ».

Далі маємо:

2. ("X) F (x) Ù (" x) H (x) = ("x) (F (x) Ù H (x))

($ X) F (x) Ú ($ x) H (x) = ($ x) (F (x) Ú H (x)).

Це означає, що квантор "володіє дистрибутивність щодо Ù, а $ - щодо Ú.

З іншого боку:

("X) F (x) Ú (" x) H (x) ¹ ("x) (F (x) Ú H (x)).

($ X) F (x) Ù ($ x) H (x) ¹ ($ x) (F (x) Ù H (x)).

Це легко показати. Нехай для першого виразу x визначений на множині D = {а, б, в}, при цьому істиною є F (а), F (б), H (в). Тоді ліва частина не виконується, а права істинна. Насправді справедливо:

("X) F (x) Ú (" x) H (x) ® ("x) (F (x) Ú H (x)).

($ X) F (x) Ù ($ x) H (x) ® ($ x) (F (x) Ù H (x)).

Сенс цих формул у тому, що опис для двох розділених предикатів не співпадає з описом, що використовують ці предикати одночасно як одне ціле і з однаковими змінними. Тому, змінивши всі змінні в їх правих частинах, отримаємо:

("X) F (x) Ú (" x) H (x) = ("x) F (x) Ú (" y) H (y),

($ X) F (x) Ù ($ x) H (x) = ($ x) F (x) Ù ($ y) H (y).

Тепер H (y) не містить змінної x і тому не залежить від зв'язування x. Звідси:

3. ("X) F (x) Ú (" x) H (x) = ("x) (" y) (F (x) Ú H (y)),

($ X) F (x) Ù ($ x) H (x) = ($ x) ($ y) (F (x) Ù H (y)).

Таким чином, процес отримання префіксной нормальної форми можна представити як послідовність кроків:

1. Використовуючи формули для ®, », замінимо їх на Ù, Ú, ¾.

2. Скориставшись виразами

внесемо заперечення всередину предикатів.

3. Вводяться нові змінні, де це необхідно.

4. Використовуючи 1, 2, 3 отримуємо префіксной нормальну форму.

В якості прикладу розглянемо такий вираз:

Шаг1:

КРОК 2:

Крок 3: немає необхідності.

Крок 4: використовуємо вираз 1 по змінної z -

Тепер застосовуємо вираз 1 по змінної w -

4.2.2.2 Скалемовская нормальна форма

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

Це означає, що якщо виділити конкретне x, то для цього x існує y, що задовольняє функції підсистема (x, y). Іншими словами, y залежить від x, тобто, якщо задано x, те й існує відповідне йому y. Звідси випливає, що y можна замінити на функцію f (x), яка задає відношення між x і y. Оскільки f (x) виникло через те, що змінна y квантифікувати $, при підстановці функції на місце y, квантор $ вже не потрібно. Таким чином, вихідну логічну формулу можна переписати: ("x) підсистема (x, f (x).

Така функція називається скалемовской.

Пріоритетність дії кванторів, наявних в префіксной формі, визначається зліва направо. Наприклад: ("x) ($ y) (" z) F (x, y, z) Þ ("x) (" z) F (x, f (x), z). А для випадку: ("x ) ("z) ($ y) F (x, y, z) Þ (" x) ("z) F (x, f (x, y), z).

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

($ X) ("y) підсистема (x, y) = підсистема.

Якщо виконати цю операцію для прикладу, отримаємо:

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

("X) ($ y) (" z) ($ w) F (x, y, z, w) = ("x) (" z) F (x, f (x), z, g (x, z)).

Якщо подібним чином виключити пов'язані квантором існування змінні, то будь-які інші змінні будуть пов'язані тільки квантором спільності і не треба пояснювати, що преременние пов'язані цим квантором. Отже, квантор загальності можна виключити. Для прикладу отримаємо:

Таке уявлення і є сколемовская нормальна форма.

Тепер можемо визначити алгоритм отримання сколемовской форми:

1. Скласти список L змінних, пов'язаних квантором спільності. Спочатку список L порожній.

2. Нехай C _i - Розглядається пропозиція, j - Номер використовується сколемовской функції S _ij. Покладемо j = 1.

3. Видалити квантори, починаючи з самого лівого і застосовуючи залежно від необхідності правила а чи б.

а. Якщо розглядається квантор "x, то видалити його і додати x до списку L.

б. Якщо розглядається квантор $ x, то видалити його і замінити x в усьому реченні C _i термо S _ij (x 1, ..., xk), де x 1, ..., xk змінні, що знаходяться в цей момент у списку L. Збільшити j на 1.

Наступним кроком є перехід до кон'юнктивній нормальній формі, а потім до клаузальной формі, тобто формі пропозицій.

Приведення до кон'юнктивній нормальній формі здійснюється заміною поки це можливо (A Ù B) Ú C на (A Ú C) Ù (B Ú C). У результаті отримаємо вирази виду A 1 Ù ... Ù An, де Ai має вигляд ( , Причому є терм або атомарний предикат або атомарна формула або їх заперечення. Доцільно здійснити і мінімізацію за такими правилами:

Нарешті, виключаємо зв'язку Ù, замінюючи A Ù B на дві формули A, B. У результаті багаторазової заміни отримаємо безліч формул, кожна з яких є пропозицією. Це і є клаузальная нормальна форма.

4.2.2.3 Пропозиції Хорна

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

Ці формули в залежності від k, l класифікуються за кількома типами.

1. Тип 1: k = 0, l = 1.

Пропозиція представляє собою одиничний предикат, і воно може бути записано як ® F (t 1, t 2, ..., tm), де t 1, t 2, ..., tm - Терми. У разі коли всі терми представляють собою константи, вони описують факти, які відповідають даним з БД. Якщо терми містять змінні, то вони задають загальнозначущі уявлення, висловлювані для групи фактів. Наприклад, такою виставою є:

® текучість (x): все тече, все змінюється.

2. Тип 2: k ³ 1, l = 0.

Цей тип можна записати у вигляді:

F1 Ù F2 Ù ... Ù Fk ®.

Зазвичай використовується для опису питання. Причина, по якій даний тип пропозиції представляється питанням, є те, що відповідь на питання реалізується у вигляді процедури докази, однак для цього докази використовується метод спростування, при якому створюється заперечення питання і доводиться, що заперечення не виконується.

3. Тип: k ³ 1, l = 1.

Цей тип відповідає запису у формі «Якщо ___, то ____.».

F1 Ù F2 Ù ... Ù Fk ® G1.

4. Тип: k = 0, l> 1.

Цей тип має вигляд:

® G 1 Ú G 2 Ú ... Ú Gl

і використовується при поданні інформації, яка містить нечіткість. Зазвичай нечіткість виникає при неповноті інформації. У цій формулі з'являється неповнота інформації в тому сенсі, що з неї не можна визначити, який з предикатів G 1, ..., Gl є істиною.

5. Тип: k ³ 1, l> 1.

Це найбільш загальний тип.

У системі пропозицій Хорна серед всіх перерахованих типів пропозицій допустимі типи пропозицій 1, 2, 3, а 4, 5 заборонені.

4.2.3Формалізація процесу доказів

Доказ демонструє, що деяка ППФ є теоремою на заданій множині аксіом S (тобто результатом логічного висновку з аксіом).

Покладемо, що S є безліч з n ППФ, а саме, A 1, A 2, ..., An, і нехай ППФ, для якої потрібно обчислити чи є вона теоремою, є B. У таких випадках можна сказати, що доказ показує істинність ППФ види:

(A 1 Ù ... Ù An ® B) (1)

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

(2)

не виконується (помилково) при будь-якій інтерпретації.

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

Основна ідея методу, званого методом резолюції, складається:

1. У перевірці містить або не містить S пусте пропозицію.

2. У перевірці виводиться або не виводиться пусте пропозицію з S, якщо пусте пропозицію в S відсутній.

Будь-яка пропозиція C _i, з якого утворюється S, є сукупністю атомарних предикатів або їх заперечень (предикат і його заперечення називаються літералами), з'єднаних символами диз'юнкції, види:

Сама ж S є кон'юнктивній формою, тобто має вигляд:

Отже, умовою істинності S є умова істинності всіх C _i в сукупності.

Умовою хибності S є хибність принаймні одного C _i. Однак, умовою, що C _i буде помилковим у який-небудь інтерпретації, є те, що безліч буде порожнім. Це легко показати. Покладемо, що це не так, тоді серед усіх можливих інтерпретацій є така, що який-небудь з літералів цієї множини або всі вони будуть істиною і тоді C _i не буде брехнею. Отже, якщо S містить пусті пропозиції, формула (2) є брехнею, а це показує, що B виводиться з групи предикатів A 1, ..., An, то є з S.

4.2.3.1 Метод резолюцій для логіки висловлювань

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

Припустимо, що в безлічі пропозицій є додаткові літерали (які відрізняються тільки символами заперечення L і ) Види:

Виключимо з цих двох пропозицій додаткові літерали і представимо частину, що залишилася у диз'юнктивній формі (таке уявлення називається резольвенти):

Після проведення цієї операції легко бачити, що C є логічним висновком C _i і C _j. Отже, додавання C до безлічі S не впливає на висновок про істинність або хибність S. Якщо виконується C _i = L, то C порожньо. Те що C є логічним висновком з S і C порожньо, вказує на хибність вихідної логічної формули.

Наведемо простий приклад такого докази:

Отримаємо доказ принципом резолюції:

- Пусте пропозицію.

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

Така структура називається дедуктивним деревом або деревом виводу.

4.2.3.2 Принцип резолюції для логіки предикатів

Оскільки в логіці предикатів всередині предикатів містяться змінні, то алгоритм докази дещо змінюється. У цьому випадку, перед тим як застосувати описаний алгоритм, буде проведена деяка підстановка в змінні і вводиться поняття уніфікації за допомогою цієї підстановки. Уніфікацію проілюструємо наступним простим прикладом.

Розглянемо два предиката - L (x) і L (a). Припустимо, що x - Змінна, a - Константа. У цих предикатах предикатні символи однакові, чого не можна сказати про самі предикатах. Тим не менш підстановкою a в x однаковими (ця підстановка і називається уніфікацією).

Метою уніфікації є забезпечення можливості застосування алгоритму докази для предикатів. Наприклад, припустимо маємо:

У даному випадку L (x) і не перебувають у додатковому відношенні. При підстановці a замість x будуть отримані, відповідно, і , І оскільки ці предикати відрізняються лише символами заперечення, то вони перебувають у додатковому відношенні. Однак, операцію підстановки не можна проводити при відсутності будь-яких обмежень.

Підстановку t в x прийнято записувати як {t / x}. Оскільки в одній ППФ може знаходитися більше однієї змінної, можна опинитися необхідно провести більше однієї підстановки. Зазвичай ці підстановки записуються у вигляді впорядкованих пар {t 1 / x 1, ..., tn / xn}.

Умови, що допускають підстановку:

• xi - є змінною,

• ti - Терм (константа, змінна, символ, функція) відмінний від xi,

• для будь-якої пари елементів з групи підстановок, наприклад (ti / xi і tj / xj) в правих чачтях символів / не міститься однакових змінних.

Уніфікація

Позначимо групу підстановок {t 1 / x 1, ..., tn / xn} через q . Коли для деякого уявлення L застосовується підстановка містяться в ній змінних {x 1, ..., xn}, то результат підстановки, при якій змінні замінюються відповідними їм термами t 1, ..., tn прийнято позначати L q.

Якщо є група різних виразів на основі предиката L, тобто L 1, ..., Lm}, то підстановка q, така, що в результаті всі ці вирази стають однаковими, тобто L 1 q = L 2 q = ... = Lm q, q - називається уніфікатором {L 1, ..., Lm}. Якщо подібна підстановка q існує, то говорять, що множина {L 1, ..., Lm} уніфіціруемо.

Множини {L (x), L (a)} уніфіціруемо, при цьому уніфікатором є підстановка (a / x).

Для однієї групи виразів уніфікатор не обов'язково єдиний. Для групи виразів {L (x, y), L (z, f (x)} підстановка q = {x / z, f (x) / y} є уніфікатором, але є також уніфікатором і підстановка q = {a / x , a / z, f (a) / y}. Тут a - константа, x - змінна. У таких випадках виникає проблема, яку підстановку краще вибирати в якості уніфікатора.

Операцію підстановки можна провести не за один раз, а розділивши її на декілька етапів. Її можна розділити за групами змінних, провівши, наприклад, підстановку {t 1 / x 1, t 2 / x 2, t 3 / x 3, t 4 / x 4} спочатку для {t 1 / x 1, t 2 / x 2}, а потім для {t 3 / x 3, t 4 / x 4}. Можливе також підстановку виду a / x розбити на дві підстановки u / x і a / u. Результат послідовного виконання двох підстановок q і l також підстановка і позначається l ° q.

Якщо існує кілька уніфікаторов, то серед них неодмінно знайдеться така підстановка s, що всі інші уніфікатори є підстановками, висловлюваними у вигляді s ° l, як складна форма, що включає цю підстановку. У результаті підстановки змінні будуть заміщатися константами і описова потужність ППФ буде обмежена.

Щоб уніфікувати два різних вираження предиката, необхідна така підстановка, при якій вираз з більшою описової потужністю узгоджується з виразом з меншою описової потужністю. Таку підстановку прийнято називати «найбільш загальним уніфікатором» (НТУ). Метод відшукання НОУ із заданої групи предикатів виразів називається алгоритмом уніфікації.

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

Покладемо, що під час перегляду послідовно всіх виразів в порядку зліва направо незбіжними термами виявилися x, t. Наприклад, отримано {L (a, t, f (z)), L (a, x, z)}. У цьому випадку, якщо:

1. x є змінною;

2. x не міститься в t, до групи підстановок додається {t / x}.

Якщо повторенням цих операцій буде забезпечено збіг всіх спочатку заданих виразів, то вони уніфіціруеми, а група отриманих підстановок є НОУ.

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

Розглянемо інший приклад:

P1 = L (a, x, f (g (y))),

P2 = L (z, f (z), f (u)).

1. Перші неспівпадаючі члени: {a, z}.

Підстановка: a / z. Маємо:

P1 = L (a, x, f (g (y))),

P2 = L (a, f (a), f (u)).

2. Перші неспівпадаючі елементи {x, f (a)}. Підстановка: [f (a) / x]. Маємо:

P1 = L (a, f (a), f (g (y))),

P2 = L (a, f (a), f (u)).

3. Перші неспівпадаючі елементи {g (y), u}. Підстановка: [g (y) / u]. Отримуємо збіг. Отже, НОУ: [a / z, f (a) / x, g (y) / u].

Алгоритм докази

Нехай задані:

Предикати робляться додатковими з допомогою підстановки [a / x]. Судження про те, чи стають два вирази додатковими, виноситься:

1. По розбіжності використовуваних символів.

2. За існуванню НОУ для двох виразів, в яких видалені однакові символи.

Далі все робиться рекуррентно.

Приклад 1. Міліція розшукує всіх в'їхали в країну, за винятком дипломатів. Шпигун в'їхав у країну. Однак, розпізнати шпигуна може тільки шпигун. Дипломат не є шпигуном.

Оцінимо висновок: серед міліціонерів є шпигун.

Скористаємося наступними предикатами:

В'їхав (x): x в'їхав у країну.

Дипломат (x): x - дипломат.

Пошук (x, y): x розшукує y.

Міліціонер (x): x - Міліціонер.

Шпигун (x): x - Шпигун.

Якщо виразимо через ці предикати посилку і висновок у формі ППФ, то отримаємо:

для всіх x, якщо x не є дипломатом, але в'їхав в країну, знайдеться міліціонер y, який його розшукує.

Якщо існує шпигун x, який в'їхав в країну, і деякий y розшукує його, то він сам шпигун.

Для всіх x справедливо, що якщо x є шпигуном, то він не дипломат.

Висновок:

Існує x такий, що він є шпигуном і міліціонером.

Якщо ці формули перетворити на клаузальную нормальну форму, то отримаємо:

Висновок перетворимо в своє заперечення:

і потім в клаузальную форму без квантора спільності.

Подальший процес доказу має вигляд:

дипломат (а) Ú міліціонер (f (а)) [a / x] з 2,4 (9)

міліціонер (f (а)) [a / x] з 8,9 (10)

дипломат (а) Ú пошук (f (а), а) [a / x] з 1,4 (11)

пошук (f (а), а) [a / x] з 8,11 (12)

шпигун (f (a)) [a / x] з 12,5 (13)