автореферат диссертации по документальной информации, 05.25.05, диссертация на тему:Машиннi методи побудови виведення у деяких некласичних численнях

Рїб од

\ 1\ 111011 іЗ^адемІя наук України Інститут кібернетики імені В. М. Глушкова

На правах рукопису

УДК 007::159.955

РОМАНЕНКО Ігор Борисович

МАШИННІ МЕТОДИ ПОБУДОВИ ВИВЕДЕННЯ У ДЕЯКИХ НЕКЛАСИЧНИХ ЧИСЛЕННЯХ

05.25.05 — інформаційні системи та процеси

Автореферат дисертації на здобуття вченого ступеня кандидата технічних наук

Київ 1993

Робота виконана в Інституті кібернетики імені В. М. Глуш-кова АН України. '

Науковий керівник: доктор технічних наук, професор КОВАЛЬ В. Н..

Офіційні опоненти: доктор технічних наук, професор

Провідна установа: Київський політехнічний інститут.

год. на засіданні спеціалізованої вченої ради К 016.45.05 при Інституті кібернетики імені В. М. Глушкова АН України за адресою:

252207 Київ 207, проспект Академіка Глушкова, 40.

З дисертацією можна ознайомитись у науково-технічному архіві інституту.

Автореферат розісланий «. 199 3 р.

ЛІТВІНОВ в. в.,

кандидат фізико-математичних наук ДЕГТЯРЬОВ А. І.

Захист відбудеться

Учений секретар спеціалізованої ради

РЕВЕНКО В. Л.

ЗАГАЛЬНА ХАРАКТЕРИСТИКА РОБОТИ

Актуальність теми. Останнім часом відмічається швидке зростання кількості застосувань математичної логіки в Інформатиці. Як приклади можна назвати логічне програмування, японський проект ЕОМ п'ятого покоління, ігродукційні експертні системи, засоби для верифікації й аналізу програм та 1н. В Інформаційних системах досягнення математичної логіки можуть використовуватися для формалізації знань експертів, для аналізу складних запитів, при побудові наслідків, що спираються на Інформацію, яка зберігається у Інформаційній системі, а також при розробці Інтерфейсу людина/ЕОМ, ¡до реалізує обмежену підмножину природної -мови. При цьому активно використовуються як класична логіка пераого порядку, так 1 некласичні логіки. В ряді випадків використання шкласичних логік має Істотні переваги у порівнянні з використанням класичної логіки, оскільки у некласичних логіках, як правило, використовуються спеціальні механізми побудови виведення, моделювання яких за допомогою стандартних засобів може призвести до істотного зростання об'єму роботи. Останнє, по суті, може позбавити нас можливості розв'язувати реальні задачі за припустимий час, навіть з використанням обчислювальної техніки.

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

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

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

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

УЗДкова новизна. У роботі отримано такі нові результати: побудовано числення революційного типу для ДСМ-логіки 1 доведено його коректність та повноту;

побудовано числення революційного типу для ситуаційної логіки і доведено його коректність та повноту;

введено та обгрунтовано поширені 'Правила поглинання та факто-ризації для побудованих числень;

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

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

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

Запропоновані модифікації правил поглинання та факторизації можуть істотно підвищити ефективність процесу побудови виведення.

Реалізація результатів досліджень. На базі результатів, отриманих у роботі, автор створив програми побудови революційного виведення як для ДСМ-логіки, так і для ситуаційної логіки. Опису основних алгоритмів цих програм 1 експериментів з ними присвячено третій розділ роботи. Програма побудови резолюційкого виведення для ДСМ-логіки входить як складова частина до експертної системи з аналізу протипухлинної активності фармакологічних препаратів, яку розроблено у ВІНІТІ РАН.

Публікації і апробація роботи. Основні результати дисертації опубліковано в роботах 11-71. Вони доповідались на семінарах товариства Курта Гьоделя (Відень), механіко-математичного факультету ОДУ й Інституту кібернепіки їм. В.М.Гдушковз АН України. Програмна система демонструвалась на виставці Всесоюзної конференції з штучного інтелекту (Мінськ, 1990) і на міжнародній конференції з логічного програмування та автоматизації міркувань (Санкт-Петербург, 1992). .

Структура роботи. Дисертація складається з вступу, трьох розділів, закінчення, списку літератури 1 додатку.

ЗМІСТ РОБОТИ

У вступі розглядається історія питання, наводиться огляд літератури.

роботи присвячено методу резолюцій для ДСМ-логіки. ДСМ-матод було розроблено у ВІНІТІ АН Росії групою під керівництвом В.К.Фінна. Головна мета розробки - формалізація міркувань, що містять в собі висування й оцінку Г-.ютез, Яі* 1 базуються на деякій множині експериментальних фактів вигляду "об'єкт X має мнокину властивостей У". Тоді гіпотези можуть змістовно розумітися як твердження вигляду "ПІДОб'ЄГ" X' е причиною наявності (відсутності) множини властивостей У'-". Якщо маємо сукупність гіпотез, то можемо прогнозувати (довизначати) властивості об’єктів, базуючись на наявності або відсутності у ¡та иідоо'ектів.

Далі можна породжувати нові гіпотези, якщо розглядати вихідні 1 довизначені об'єкти 1 намагатися довизначити нові об'єкти. Кажуть, що ДСМ-вивід закінчено, якщо на черговій Ітерації не довизнача-ється жоден об'єкт. ’ ’

Зрозуміло, що як твердження про наявність/відсутність властивостей у об'єктів, . так 1 твердження, що відповідають гіпотезам, мусять мати вирізнені логічні статуси. Цього можна досягти, змінивши спосіб оцінки предикатшх символів. А саме: нехай Л - непорожня скінченна множина, елементи якої будемо звати істинносними значеннями, Л - множина невід'ємних цілих чисел. Тоді значенням оцінки в на атомі Р(...) (де Р - предикатний символ) буде пара <\,п>, де \ е Л - логічний статус ствердження, а п е И - номер Ітерації.алгоритму, на якій ствердження отримало цей статус. Пре-дикатні символи, що оцінюються таким чином, будемо звати "кольоровими" (оскільки \ можна вважати "кольором", а п - його насиченістю). Поряд з ними до формул можуть входити 1 звичайні ("чорно-білі") предикати або формули, що оцінюються тільки в Істину або хибність в класичному їх розумінні.

Змістовна трактовка може бути, наприклад, такою. Розглянемо А = {-1, 0, 1, т), причому -1 відповідає "експериментальній хибності", 0 - "суперечності", 1 - "експериментальній істині" і х -"невизначеності". Тоді значення оціїши, що дорівнює <-1,0> на твердженні вигляду X У (де =»] - кольоровий предикатний символ, який розглядається як "мати властивість") означає, що на нульовій ітерації (тобто до того, як застосовувався ДСМ-метод) твердження про те, що об'єкт X мав множину властивостей У мало статус "експериментальна хибність”. Іншими словами, серед вихідних експериментальних фактів був факт про те, що об'єкт X не має множини властивостей У. Значення оцінки, що дорівнює <1,1>, на тпержденні того ж. вигляду означає, що на першій ітерації було отримано прогноз про те, що об'єкт X повинен мати множину властивостей У. Нарешті, значення оцінки <т,2> свідчить, що на другій Ітерації не вдалося спрогнозувати наявність/відсутність мноїмни властивостей У у об'єкта X. Інший кольоровий предикатний символ - =*2 ("бути причиною") використовується для запису гіпотез про причини наявності/

відсутності властивостей. Наприклад, (твердження вигляду X' оцінюється у <-1,1>, якщо на першій ітерації було породжено гіпотезу, що підоб’єкт X' є причиною відсутності множини властивостей Y'.

Звичайно, мову ДСМ-логіки розширюють двома операторами, а саме: .1^ 1 .1^ П), які застосовуються лише до кольорових

атомів. Значенням оцінки на формулі .1^ п>?(...) буде Істина тоді

1 тільки тоді, коли значення цієї ж оцінки на атомі Р(...) дорівнює <\,п>. В усіх Інших випадках значенням оцінки на формулі ^<\ е и0н1сть> Значенням оцінки на формулі .1^ П^Р(...)

буде Істина тоді 1 тільки тоді, коли значення цієї ж оцінки на атомі Р(...) дорівнює <Х,к> 1 к < п.. В усіх Інших випадках значенням оцінки на формулі 3 ^ п)р< ■' ’ > 0 хийн1сть- Таким чином, формула, яка містить ^оператор на верхньому рівні, є чорно-білою. Наявність ^операторів дозволяє записати деякі цікаві твердження, наприклад: .

Уп( (,І<-1 ,п>х=>1у 7 *г<0,п>х,’ії у ,І<1 ,п>х=>1У) ^ 1,І<т,тІ>Хг’іУ)

означав, що об'єкт не може "втратити" своїх властивостей.

Наведений вище формалізм може застосовуватися для побудови, так званого правдоподібного виведення. Наведемо як приклад один з найпростіших його варіантів. Нехай об’єктам відповідають множини, ь розглядувані множини властивостей одноелементні (останнє, по суті, не є обмеженням). Процес побудови виведення складається з послідовності ітерацій, кожну з яких розіб'ємо на дві фази. У першій фазі (породження гіпотез) для кожної властивості у розглядаються всі твердження вигляду .Т,, ^(Х =»1 у), де к < п, п - номер ітерації. Для цих тверджень будуються всі непорожні максимальні перерізи X" мнокин у лівій частині 1 до сукупності тверджень додаються твердження .1^ П>(Х' =», у) (позитивні гіпотези). Аналогічно по множині тверджень вигляду к>(Х у) будуються

негативні гіпотези (твердження вигляду *9 у)). Далі,

якщо існують позитивна 1 негативна гіпотези з однакового! лівою та правою частинами, то обидг.І ці гіпотези викреслюються, а до сукупності тверджень додається твердження вигляду .^д П>(Х' »2 У)

(суперечлива гіпотеза). ■

У другій фазі (довизначення фактів) для кожного твердження вигляду )(Х =■, у) шукаються-позитивні (або негативні) гіпотези в2 (відповідно П>(Х' =>2 у)), такі, що

X' с X. Якщо знайдено лише позитивні (відповідно негативні) гіпотези, то твердження .7^ п_і)(Х у) замінюється на <1^ П>(Х =»1 у) (відповідаю П>(Х ^ у)). Якщо знайдено гіпотези обох знаків,

або відповідні гіпотези не існують взагалі, то твердження <г('с,п-1)(Х ”1 замінюється на ^ }(Х =»1 у). '

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

\/п Ух Vy ( 0>(х =»1 у) ■» -і( Зг Зіи ( (г, с и) & = 0) &

& (и с у) & 1(1» = 0) &

& ( «^„-І >п>(2 =»2 у

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

Як зазначалося вище, для розв’язання схожих гпдач звичайно використовується метод резолюцій. Побудові його аналогу для ДСМ-логіки присвячено перший розділ. Загальновідомо, що об'єктами виведення в революційному численні для класичної логіки є диз'юнкти, що розглядаються як множини літер. Аналогами літер для ДСМ-логіки можуть бути вирази вигляду |Л,п-,Р(...) та гЛ,л-,Р(...), де Р(...) -кольоровий атом (основа літери), X е. А, п € N. Вирази 1-А.,п-) та іЛ,п-, звичайно звуть знаками літер. Кажуть, що оцінка 0 справджує літеру іА,гМР(.. ■), якщо її значення на ?(...) дорівнює <Л,к>, причому к > п. Відповідно, оцінка в справджує літеру Г\,п-,Р(...), лкцо її значення на Р(...) дорівнює <А.,к>, причому к < п. Літери

Ь| 1 І>2 звуть контрарними, якщо жодна оцінка не справджує їх одночасно. Зауважимо, що контрарні літери повинні мати уніфікусмі (в звичайному розумінні) атоми. Диз’юнкти для ДСМ-логІки визначаються як множини літер, що розуміються як диз'юнкція літер. Диз'юнкт, що складається з порожньої множини літер, зветься порожнім диз’юнктом. Можна-довести, ідо довільна ДСМ-формула може бути зведена до еквівалентної множини диз'юнктів, яка розуміється як кон'юнкція диз'юнктів. _

Бінарною резольвентою диз'юнктів В] та В2, таких, що Б1 = (І|) и 1 Б2 = и Б2'. контрарна до і найбільш загальний уніфікатор основ ЬІ і дорівнює о, назвемо диз’юнкт (В^' и В2')о. Фактором (зклейкою) диз’кщту Б = (Ь1} и (І^) и ... II (1^) и Б', к. > 1, такого, що І^,...,^ мають однакові знаки 1 уніфікуємі з найбільш загальним уніфікатором о, назвемо диз’юнкт ({1^} І) В' )о. Нарешті, резольвентою диз'юнктів та В2 _ (Я(ВІ ,0-,)) назвемо їх бінарну резольвенту, або бінарну резольвенту їх факторів. •

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

Правило резолюцій. Нехай Д - множіта диз'юнктів, € Д, В2 € Д 1 Існує резольвента И^^)- Тоді дозволяється додати 11^,Б2) до Д. Якщо на якійсь ітерації цього процесу ми отримаймо диз'юнкт Б, то будемо казати, що Б виводиться з Д.

Істотною особливістю методу резолюцій для ДСМ-логіки с наявність потенційно нескінченної множини літер з однією 1 ТІЄЮ ж основою, але різними знаками. Дня того, щоб зрозуміти, як це може вплинути на метод резолюцій, розглянемо простий приклад. Нехай V -пропозиціональна змінна, а (нескінченна) множина Д складається а

таких диз'юш<тів:{і-\1СУР), <ча,2^'....... Певна річ,

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

Головним результатом першого розділу с така теорема, що стверджув повноту методу резолюцій:

Теорема. Скінченно різноманітна множина диз'юнктів суперечлива тоді і тільки тоді, коли з неї можна вивести порожній диз'юнкт. , .

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

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

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

Решту першого розділу присвячено розгляду формул, які мають вигляд

■ Уп Ут ( ь1 (п) ф Ь^т) ),

де (п) та І^Ст) - літери, які містять п і в в знаках, а ер - або кон'юнкція, або диз'юнкція. Для більшості таких формул наводяться еквівалентні формули, до яких не входять піт. Важливість розгляду пов'язана, з одного боку, з тим, що формули, які мають вищезазначений вигляд, часто зустрічаються в множині диз'юнктів, а

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

ЙВїШ* розділ присвячено розгляду так званої ситуаційної логіки. Ця логіка, розроблена К.П.ВершинІним, призначена для формалізації міркувань експерта у важкоформалізуємих предметних галузях. Головною одиницею знань, вмінь та навиків експерту при цьому вважається ситуація, що розглядаєься як сукупність тверджень, понять, Імперативних процедур, прикладів розв’язання задач та прецедентів (прикладів застосування процедур до розв'язання задач). Прикладом такої ситуації може бути проектування житлового будинку. Певна річ, твердження, які е Істинними в одній ситуації, можуть бути хибними в іншій (не можна проектувати' мікрорайон точнісінько так, як проектується один будинок). Крім Того, в ситуації можуть бути здійснені дії,- які, можливо, переводять її в Іншу ситуацію. На множині ситуацій задаються два відношення: "бути більш загальною" та "бути підпорядкованою”. Ситуація S є більш загальною ніж ситуація S', якщо кожне твердження, істинне в S, є істинним 1 в S'. Ситуація S є підпорядкованою ситуації S', якщо коша дія, що змінює S (тобто переводить її в іншу ситуацію), змінює 1 S'. Таким чином, ми одержуємо ситуаційну структуру, що становить множину ситуацій з заданими на них відношеннями "бути більш загальною" та "бути підпорядкованою". В роботі Вершиніна та Гергея (1990) наводиться логічний формалізм SSL, який дозволяє, зокрема, виразити властивості ситуацій і ситуаційних структур. ■ ■

Обмеження SSL на випадок, коли ситуаційна структура складається з однієї ситуації розглядається в [61. Таке'обмеження (SSLg)’ може бути використане для опису ситуацій "зсередини". Головною його відмінністю від класичної логіки є запровадження третього істинносного значення, що розглядається як "невизначеність” ("незнання"). Введення третього істинносного значення дов’язане з необхідністю розгляду питання про істинність тверджень, які

містять поняття, невідомі в даній ситуації. Отже, оцінка предикатного символу в ББІд може приймати одне з трьох значень: О (хибність), Л (невизначеність) і 1 (істина). Ці значення вважаються упорядкованими тазам чином: О < Л < 1.

Мова ББЬд відрізняється від мови класичної логіки предикатів наявністю нової зв'язки: ~ (інволюція). Кон'юнкція та диз'юнкція розглядаються^- відповідно, як мінімум та максимум в розумінні вказаного вище порядку. Нижче наведено таблиці Істинності для заперечень -та імплікації:

1 А І іА ! ~А І ’! А 0 0 0 л л л 1 1 1 !

І В 0 Л 1 0 л 1 0 л 1 !

іоі 1 ; 1 І ! А«В 1 1 1 0 1 1 0 л 1 !

І Л І О І Л І

111 0 1 0 1

Квантори- загальності та Існування розглядаються, відповідно, як нескінченні кон'юнкція та диз'юнкція. •

Першу частину другого розділу присвячено розгляду таких понять, як логічний наслідок, справдауваність та суперечність відносно SSXjq". Виявляється, що логічний, наслідок можна визначити одним а чотирьох шляхів, а саме: ■

'■ Г *>. F « V8( min 6(Е') = v и 6(F) = v' •» v ^ ч' )

• 1 F'ir

Г і=2 F * V0( VF'er ( 0(F') = 1 ) » 0(F) = 1 )

.. Г >=з F «■ V0( VF'ЄГ ( 0(F' ) * 0 ) => 0(F) V 0 )

Г >=4 F •» V0 ( VF' eT ( 0(F’ )*1 ) V e(F)^0 )

де Г - множина формул; F та F' формули; v та v' -логічні значення; Є - оцінка. Варто зауважити, що Г *2 F 1 Г F, тоді 1 тільки

тоді, коли Г F, а такоу що Г ^ F або Г »=3 F, тягне за собою

Г F.

Далі, у відповідності до кожного з означень логічного наслідку ми можемо визначити справджуваністі 1 суперечність формули.

Означення І. Оцінка в справджує формулу F в розумінні (*2). якщо 9(F) = 1. Оцінка 0 справджує формулу F в розумінн1 *=3 (*4), якщо в(Р) t Cu,1). '

Таким чином, виявляється, що поняття справджуваності формули залежить від поняття логічного наслідку, тому надалі .ми будемо казати, що "формула справджується в розумінні *=3, *=4).

Можливі різні означення суперечливості, а саме:

• Означення 2. Суперечливою зветься множина формул, яка не справджується жодною оцінкою.

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

Можна довести, що у випадку та мз Ш означення суперечливості "рівнооб’ємні", тобто формула є суперечливою у відповідності з одним з цих означень тоді 1 тільки тоді, коли вона суперечлива у відповідності з іншим. Для ^ та ця властивість не виконується, тому в решті другого розділу розглядаються лише *2 та *3. ^

Як відомо, для методу резолюцій Істотною є зводимість питання, чи є Формула логічним наслідком множини формул до питання про суперечливість множини формул. Така зводимість існує лисе для *=2 ^ ^ ^2 *

Теорема. Г г 1 тільки тоді, коли Г и (п З?) суперечливе в розумінні *2*

Теорема. Г ? тоді 1 тільки тоді, коли Г и суперечливе В розумінні 1=3. • .

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

?, ~¥, іР, і~Р, пР, ~п~Р . ,

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

Легко довести, що формула справджується в розумінні ^ тоді 1 тільки тоді, коли справджується (в розумінні *2) формула

-iF. Кожна також довести, що формула F справджується в розумінні ^ тоді і-тільки тоді, коли справджується формула -TF. Тому достатньо обмежитися розгляд м чотирьох типів літер, а саме: ■ ’

Р(...). ~Р(...), -пР(...), т“Р(...)

Аналогічно, якщо розглядати справджуваність 1 суперечність у розумінні pg, -достатньо розглянути такі чотттри типи літер:

Р(...), ~Р(...), пР(...), і"?(...)

’ "Як і в класичному випадку, контрарішми звуться такі літери, які не справджуються одночасно жодною оцінкою. Тоді ми можемо зформулювати два правила резолюцій: (для ^ і відповідно). Відповідні формулювання збігаються з наведеними віще для ДСМ-логіки. Головним результатом другого розділу е така Теорема. Множина диз'юнктів суперечлива в розумінні >=2 ("=3) тоді 1 тільки тоді, коли з неї за допомогою правила резолюцій можна вивести порожній диз'юнкт. Доведення цієї теореми провадиться за допомогою•семанилних дерев.

. В заключній частині другого розділу розглядаються поширення понять факторизації та поглинання для SSLQ. Як 1 для ДСМ-логІки, вдається відмовитися від вимоги про повний збіг знаків склеюваних літер. .

• у ТБ§тьому розділі розглядається комплекс- програм, що реалізують процес побудови виведення для ДСМ-логіки та SSLg. ЦІ програми було реалізовано на ПЕОМ ІВМ/РС під керуванням операційної системи MS DOS. Докладно описано алгоритми та структури данних, які застосовано в цих програмах.

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

сопсаг((Х.Ь),Ь1) -> ІХ.сопсаиЬ.ЬІ)] .

сопсаКпІІ.ЬІ) -> Ь1 . .

У програмі для ДСМ-логіки переписування термів використовується для реалізації операцій над множинами.

. У програмі для ББІд, у порівнянні з програмою для ДСМ-логіки, наявні додаткові особливості, що поширюють 11 можливості:

1. Гнучкий синтаксис, який дозволяє використовувати префіксну,

інфіксну та міксфіксну форми запису. •

2. Можливість роботи з багатосортними сигнатурами, на сортах яких .

задано частковий порядок. (Відповідно, реалізовано багатосортні варіанти таких алгоритмів як уніфікація та порівняння Із зразком). ■ • ' '

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

4. Реалізовано загальновживані сорти (типи Даних): цілі, символи,

послідовності символів. Константи цих сортів зберігаються у машинному вигляді, а не у вигляді абстрактних термів, що Істотно економить;,пам'ять. При уніфікації (порівнянні Із зразком) дозволяється зіставляти константу одного з цих сортів з абстрактним термом цього сорту. ■

5. Користувач може написати свої власні програми-на процодурній мові програмування для виконання операцій над константами сортів, які розглядаються у п. 4. Наприклад, можна написати 'програми, що реалізують цілочисельну арифметику.

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

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

Заключну частину третього розділу присвячено Інтерфейсу

користувача. Розглядається Інтегроване оточення LWB (Logician'в Workbench) [7], куди входять ряд програм доведення теорем для класичної логіки те вищезгадані програми. Головною метою розробки LWB було створення комфортного оточення для користувача. Імена. файлів з даними, конкретний. тип програми для доведення теорем та

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

■ J3-Іншого боку,- програми можуть працювати 1 автономно, а також '

в складі Інших програмних систем. В останньому випадку може видатися корисним вимкнути’вивід інформації на екран, щоб зробити роботу прогргчи "прихованою". ■

Список літератури.

1. Крмплекс программ для экспериментов с выводами революционного типа / А.В.Брановицкий, К.П.Вершинин, Д.М.Райко, И'.Б.Романенко,

‘ А.А.Сахно // Тез. докл. II Всесоюз. конф. по прикладной логике, 7-9 июня 1988 Г. - Новосибирск, 1988. - С. 25-26.

2.- Вершинин К.П., Романенко И.Б. Программа построения вывода для

ДСМ-логики // II Всесоюз. конф. "Искусственный интеллект-90". -Минск, 1990. - С. І60-І6І. •

3. Вершинин К.П., Романенко И.Б. Распространение метода резолюций

на некоторые недвузначные логики // Семиотика и информатика. -1990. - Вып. 31. - С. 104-123 '

4. Вершинин К.П., Райко Д.М.. Романенко К.Б. Комплекс средств анализа экспертных систем // Выставка программных средств. -Киев: Коммерческий центр Института кибернетики им. В.М.Глушкова All Украины, 1990. - ч. I. - С. 15

5. Rajko D., Vershinin K., Romanenko I. Algebraic Program

Interpreter aPREX2 // Lect. Notes Comput. Scl. - 1991. - 480. -P. 547-548. ‘ '

6. Vershinin K.P., Romanenko I.B. One more logic with uncertainty

and resolution principle Гог It // lect. Notes Comput. Scl. -1992. - 607. - P. 663-667 '

7. Romanenko I.B. Logician’s Workbench // Lect. Notes In

Artificial Intelligence. - 1992. - 624. - P. 499-500.