10. Формальні теорії

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

В алфавіт мови системи входять предметні константи, предметні змінні, предикатні константи, предикатні змінні, логічні зв'язування й квантори, допоміжні символи (дужки, коми тощо).

Множина слів мови складається із правильно побудованих формул (ППФ). Це аксіоми, що задаються насам­перед при побудові теорії. Правила виведення дозволяють одержувати з аксіом нові ППФ – теореми. Множина аксіом називається незалежною, якщо ні одну з них не можна, вивести із сукупності інших. Часто для спрощення доказу теорем у систему аксіом включають і залежні.

Безпосередня виводимість F з Fi,F₂,...,F_n записується у вигляді ------------- . Над рисою записуються передбачувані істинними посилки, під рисою – висновок). Факт виводимості позначається Fi,F₂,...,F_n \- F. Мітка d служить для посилань на правило.

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

Логічне вирахування будемо називати несуперечливим, якщо в ньому не виведені одночасно F і F . У супе­речливих вирахуваннях виведена будь-яка формула. Остання обставину можна використати для доказу несуперечності вирахування: досить показати існування в ньому невиведеної формули.

11. Процедура резолюції

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

У сучасних системах автоматизації логічного виведення широко використається метод резолюцій. У проце­дурі резолюцій замість заданої формули F, передбачуваної тотожно істинною, розглядають її заперечення -iF і на­магаються довести його суперечливість. Це власне кажучи "доказ від противного". У його основі лежить операція виключення з різних пропозицій висловлень-резольвент, якщо ці висловлення в одних пропозиціях заперечують­ся, а в інших - ні. Необхідна суперечливість встановлюється як одночасна справедливість двох взаємовиключних висловлень. Якщо процес виведення резольвент обірветься, не привівши до протиріччя, то вихідна теорема невір­на. Достоїнством методу резолюцій є можливість виявлення протиріччя набагато раніше, ніж буде виконаний пов­ний перебір можливостей. Розроблено багато евристичних поліпшень спрямованості й тим самим - швидкодії ме­тоду.

Спочатку запишемо відомі істинні факти у вигляді логічного добутку диз'юнктивних форм:

1. BvA

2. CvB

3. С

Допустимо, що ми хочемо довести А. Щоб це зробити, доповнимо заданий набір запереченням А:

1. BvA

2. CvB

3. C

4. A

Виключимо тепер знову введене речення і його заперечення в іншому реченні. Цей процес називається ре­золюцією (може бути, тому, що резолюції найчастіше негативні??). Наприклад, ми можемо виключити А й А в

першому, залишивши в них без зміни сукупність інших висловлень (таку сукупність називають резольвентою). У результаті залишаються

1. В

2. CvB

3. С

Тепер виключимо В в першому реченні й В ­– у другому:

1. С

2. С

Крім обох залишившихся речень, одержуємо порожнє речення, що означає істинність А. Правила виведення представляються як В D Е -> А (хорновські диз'юнкти).

Вибір пари речень, що зіставляються при виборі чергової резольвенти, реалізується в ієрархічно організова­ному просторі станів - дереві І/АБО на основі стратегії "углиб, починаючи ліворуч". Задана мета Р зіставляється з першим реченням, що має Р у якості висновку. Потім доводиться перший компонент відповідного диз'юнкта, і т.д.