ПРОГРАМНЕ ЗАБЕЗПЕЧЕННЯ ІНТЕЛЕКТУАЛЬНИХ СИСТЕМ

Правила ІІ роду.

Означення 5.

Позитивна або (+)-гіпотеза ІІ роду, отримана за правилом П+, є той об’єкт НΩτ, для якого існує (+)-гіпотеза І роду така, що h+H та для довільної (–)-гіпотези І роду має місце h–H.

Негативні (або (–)-) гіпотези визначаються двояко. НΩτ називається суперечливою (або (0)-) гіпотезою, отриманою за правилом П0, якщо Н включає голови як позитивних, так і негативних гіпотез І роду.

Розмірковування.

Вивід правдоподібних гіпотез в ДСМ-методі здійснюється в рамках квазіаксіоматичних теорій (КАТ). КАТ є трійка

<, , >,

де  – множина аксіом, що неповно описує предметну область (ПО),  – множина емпіричних елементарних речень про об’єкти з ПО. Зазвичай вони відповідають твердженням вигляду “Об’єкт має властивість А”. Множина  відкрита та може поповнюватися за рахунок проведення нових експериментів, спостережень та ін.,  – множина правил виведення.  = 10, де 1 – множина правил правдоподібного виведення (ППВ) та 0 – множина правил достовірного виведення.

Розмірковування в КАТ є побудова ланцюжка формул 1, …, n, де кожна і або аксіома з , або фактичне висловлювання з  (відповідає (+)- чи (–)-прикладу – тобто об’єкту з ?+ чи ?–), або отримана з попередніх формул ланцюжка 1, …, n шляхом застосування правил з  як, наприклад, гіпотези І та ІІ роду. Визначення розмірковування в КАТ відрізняється від визначення логічного виведення тим, що:

1. – відкрита множина, елементи якої і, релевантні цілі n, вставляються в ланцюжок, якщо має місце відношення схожості цілі – і R n.

2.Серед правил , що застосовуються при побудові вказаного ланцюжка формул, є правили з  , де  – множина правил правдоподібного виведення.

3.В процесі побудови ланцюжка 1, …, n можуть використовуватися металогічні засоби, наприклад, перевірка на несуперечливість, на невиводимість, на виконуваність або невиконуваність деяких умов та ін.

Множина аксіом  складається з множини процедурних аксіом pr та множини декларативних аксіом dc. Аксіоми з pr формально виражають собою застосування правил І та ІІ роду з врахуванням їх часткового впорядкування. Частина декларативних аксіом з dc (позначимо її dc0) описує структуру даних (алгебру схожості, сполучення та різниці) предметної області, що розглядається. Інша частина декларативних аксіом, dc1, описує деякі природні властивості причинних відношень та гіпотез про них: правила комбінації наслідків одних і тих самих причин, а також принципи казуальної несуперечливості та повноти.

Нехай правила І та ІІ роду, що застосовуються в ході ППВ, фіксовані. Тоді вимогою аксіоми (принципу) казуальної несуперечливості полягає в тому, щоб (+)-приклад не міг би стати (–)-гіпотезою ІІ роду на якому-небудь кроці породження гіпотез. Аксіома казуальної повноти вимагає того, щоб усі (+)-приклади ставали (+)-гіпотезами ІІ роду на якому-небудь кроці породження гіпотез.Декларативні аксіоми ДСМ-методу можуть бути засобом керування розмірковуванням: при невиконанні якої-небудь аксіоми ДСМ-“розмірковувач” може вимагати поповнення бази даних новими прикладами та вказувати вид прикладів, що дозволяють добитися виконання аксіоми після застосування ДДСМ-ППВ. Перевірка виконуваності аксіом може здійснюватися часто дедуктивним шляхом з використанням засобів логічного виведення, основаних на логічній теорії ДСМ-методу. Система логічного виведення інтегрована з засобами правдоподібного виведення ДСМ-методу в єдину логіко-інформаційну обчислювальну систему та дозволяє отримувати дедуктивний доказ або спростування виконання тих чи інших залежностей на об’єктах та гіпотезах із ДСМ-бази даних. Об’єднання в ДСМ-розв’язувачі індуктивного та дедуктивного виведення дає можливість бачити схожість ДСМ-розмірковувань з навчанням в системах, основаних на поясненні: складні залежності на об’єктах з бази даних є тут аналогами тверджень, що не задовольняють критерію операціональності. “Навчання” їм можливо лише після навчання елементарним гіпотезам (тобто отримання їх за допомогою правил І та ІІ роду) та проведення на їх основі логічного виведення.