Повні методи пошуку виведення в системах логічного програмування

Размещено на http://www.allbest.ru/

КИЇВСЬКИЙ НАЦІОНАЛЬНИЙ УНІВЕРСИТЕТ

ІМЕНІ ТАРАСА ШЕВЧЕНКА

Автореферат

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

кандидата фізико-математичних наук

Спеціальність: 01.05.01 - Теоретичні основи інформатики та кібернетики

Повні методи пошуку виведення в системах логічного програмування

Афонін Андрій Олександрович

Київ 2011

Дисертацією є рукопис.

Робота виконана в Національному університеті «Києво-Могилянська академія».

Науковий керівник: доктор фізико-математичних наук, професор Глибовець Микола Миколайович, Національний університет «Києво-Могилянська академія», декан факультету інформатики

Офіційні опоненти: доктор фізико-математичних наук, професор Клименко Віталій Петрович, Інститут проблем математичних машин і систем НАН України, м.Київ, заступник директора з наукової роботи

кандидат фізико-математичних наук, с.н.с. Лялецький Олександр Вадимович, Київський національний університет імені Тараса Шевченка, факультет кібернетики, старший науковий співробітник

Захист дисертації відбудеться «23» червня 2011 р. о 14 годині на засіданні спеціалізованої вченої ради Д 26.001.09 Київського національного університету імені Тараса Шевченка за адресою: 03680, м. Київ, проспект академіка Глушкова, 4д, факультет кібернетики, ауд. 40.

З дисертацією можна ознайомитись у Науковій бібліотеці ім. М. Максимовича Київського національного університету імені Тараса Шевченка за адресою: 01033, м. Київ, вул. Володимирська, 58.

Автореферат розісланий «23» травня 2011 р.

Вчений секретар спеціалізованої вченої ради Шевченко В.П.

1. Загальна характеристика роботи

логічний програмування пошук елімінація

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

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

Зв'язок роботи з науковими програмами, планами, темами. Наукові результати роботи отримані в рамках наукових тем «Розробка принципів застосування інтелектуальних агентів в інформаційних системах» (2005-2009, № державної реєстрації 0105U006983) та «Створення програмної платформи підтримки автоматизованої системи управління навчальним закладом» (2009-2010, № державної реєстрації 0109U000678) факультету інформатики Національного університету «Києво-Могилянська академія».

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

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

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

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

Наукова новизна одержаних результатів полягає в такому:

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

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

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

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

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

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

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

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

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

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

o VI Міжнародній конференції TAAPSD'09 (Київ, Україна, 2009);

o XI Міжнародній науковій конференції «Інтелектуальний аналіз інформації» (Київ, Україна, 2010);

o XII Міжнародній конференції «Системний аналіз та інформаційні технології» (Київ, Україна, 2010);

o VII Міжнародній конференції TAAPSD'10 (Київ, Україна, 2010).

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

Структура і обсяг дисертації. Дисертація складається зі вступу, чотирьох розділів, висновків, списку використаних джерел. Повний обсяг дисертації складає 118 сторінок, із них 110 сторінок основного тексту.

2. Перелік основних результатів дисертації

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

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

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

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

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

[B],<w1,F1,E1>,...,<wn,Fn,En> <u1,G1,E1>, …, <um,Gm,Em>,

де <w1,F1,E1>, ..., <wn,Fn,En>, <u1,G1,E1>, ..., <um,Gm,Em> - ансамблі і [B] - список ансамблів.

(Під ансамблем розуміється упорядкована трійка <w,F,E>, де w є послідовність (слово), що складається зі спеціальних невідомих і фіксованих змінних, які з'являються при пошуку виведення, F - формула першого порядку, E - множина пар термів t1 і t2).

З будь-якою а-секвенцією S пов'язується її формульний образ fi(S).

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

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

Нехай F є формула (секвенція/а-секвенція S). Тоді HQ(F) (HQ(S)) позначає наступну множину термів, названу ербранівським квазіуніверсумом формули F (секвенції/а-секвенції S): кожна константа, кожна вільна змінна й кожна позитивна змінна з F належать HQ (F) (якщо жодна константа не входить у F (S), то спеціальна константа c0 належить до HQ(F)) (HQ(S)); якщо f є k-арний функціональний символ із F (S), та t1,...,tk HQ(F) (t1,...,tk HQ(S)), то f(t1,...,tk) належить до HQ(F) (HQ(S)).

Нехай F - формула та F1,...,Fn - її варіанти. Якщо F1,..., Fn попарно не мають загальних зв'язаних змінних, то формула F1...Fn (F1...Fn) називається варіантним -дублікатом (-дублікатом) формули F.

Нехай G є формула та H є -дублікат (-дублікат) деякої формули F. Результат заміни в G формули F її дублікатом H називається однокроковим ербранівським розширенням формули G, якщо виконується така умова: F є негативною -підформулою (позитивною -підформулою) формули G та H є варіантний -дублікат (-дублікат) формули F, що не має загальних зв'язаних змінних з G.

Результат HE (G) деякої скінченої послідовності однокрокових розширень, послідовно застосовуваних спочатку до G, потім до отриманого результату і т. д., називається ербранівським розширенням формули G.

Якщо S - секвенція/а-секвенція і H1, …, Hk - деякі формули із її антецедента та/або сукцедента, то ербранівським розширенням секвенції/а-секвенції S називається секвенція/а-секвенція HE (S), отримана із S за допомогою заміщення H1, …, Hk деякими відповідними ербранівськими розширеннями HE(H1), …, HE(Hk).

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

Теорема 2.2 (а-секвенційна форма теореми Ербрана). Нехай S - вихідна секвенція, що складається тільки з замкнутих формул, і SC - деяке числення а-секвенцій з пропозиціональною частиною pSC, рівнооб'ємною пропозиціональній частині числення LK. S вивідна в численні LK тоді і тільки тоді, коли існують ербранівське розширення HE (S) секвенції S і підстановка термів з ербранівського квазіуніверсума HQ(S) замість усіх негативних змінних секвенції HE(S) такі, що: (i) можна побудувати дерево виведення Tr для секвенції (HE(S)). у численні pSC; (ii) є допустимою підстановкою для HE(S), де (HE(S)) - результат вилучення всіх кванторів із ербрановского розширення HE(S).

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

Наслідок 2.2. Замкнута універсальна (екзистенціальна) формула F є невиконуваною (загальнозначущою) тоді і тільки тоді, коли існують варіанти F1, …, Fn формули F і підстановка термів з ербранівського квазіуніверсума HQ(F) замість усіх змінних формули F1 … Fn (F1 …Fn), такі, що безкванторна формула (F1 … Fn). ((F1 …Fn).) є невиконуваною (загальнозначущою), де (F1 … Fn) ((F1 …Fn)) є результат вилучення всіх кванторів із F1 … Fn (F1 … Fn).

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

Теорема 2.3. А-секвенція S з несуперечною множиною всіх формул з її посилок вивідна в численні aS тоді і тільки тоді, коли її формульний образ fi(S) є загальнозначущою формулою.

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

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

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

У третьому розділі спочатку проводиться очевидне перетворення aS в числення saS для випадку попередньої сколемізації а-секвенції. Для побудованого saS доведено його коректність і повноту.

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

Далі вивчається так зване числення літеральних секвенцій lS - модифікований випадок saS, коли в антецеденті секвенцій знаходяться диз'юнкти, а в сукцеденті - тільки одна кон'юнкція літер, у зв'язку з чим спрощуються правила виведення числення saS. (Диз'юнкт в дисертації розглядається як упорядкована мультимножина літер, яка записується у вигляді виразу L1 ... Lk, де L1, ..., Lk - літери; пустий диз'юнкт позначається .) За допомогою теореми 3.1 доводиться, що числення lS є коректним і повним (теорема 3.2).

Числення lS дозволяє перейти до числення lT, вивідними об'єктами якого є так звані літеральні дерева, тобто дерева, вузли яких помічені літерами. Під замкненим деревом мається на увазі дерево, листя якого помічені пустою формулою #. Пусте дерево позначається .

Вихідне дерево (відносно диз'юнкта L1 ... Ln з вихідної множини диз'юнктів MI) складається тільки з кореня з міткою MI і k його спадкоємців із літерами L1 , ..., Ln.

Нові дерева будуються відповідно до правил виведення числення літеральних дерев; при цьому під виведенням в lT розуміється послідовність літеральних дерев T1,..., Tr, в якій T1 є вихідне дерево і для Tj (j > 1) отриманий з деякого варіанту попереднього дерева по одному з правил виведення. (У методах, що базуються на резолюційній парамодуляційній техніці, виведення також мають вигляд послідовностей).

Числення lT має два правила резолюційного типу RE і CC.

Правило вхідного резолюційного розширення RE. Нехай MI є вихідна множина диз'юнктів, що містить вхідний диз'юнкт D вигляду L1 ... Li ... Lk, де L1, ..., Lk - літери (k> 0). Нехай Tr є варіант деякого літерального дерева, який не має спільних змінних з D і E - його найбільш правий лист, відмінний від #. Припустимо, що до D і E застосовано правило вхідної резолюції, є породжуваний н.о.у. множини {L, ~E} і при k > 1 дерево Tr' побудоване з Tr за допомогою додавання до виділеного листа з E (k-1)-го спадкоємця з мітками L1, ..., Li-1, Li+1, ..., Lk відповідно, а в разі k = 1 дерево Tr' побудоване з Tr за допомогою додавання до виділеного листа з міткою E одного спадкоємця з # в якості його мітки. Тоді кажуть, що за правилом RE з Tr і D виводиться дерево Tr'..

Правило контрарного закриття CC. Нехай Tr є деяке літеральне дерево і Br - його найбільш права гілка з листом, що мають мітку L, відмінну від #. Припустимо, що для деякого вузла з міткою E з гілки Br існує н.о.у. множини {L,~E} і дерево Tr' побудоване з Tr за допомогою додавання до виділеного листа з міткою E одного спадкоємця з # в якості його позначки. Тоді кажуть, що за правилом CC з Tr і D виводиться дерево Tr'..

Відносно lT маємо наступний результат про його коректність і повноту.

Теорема 3.3. Нехай MI позначає скінчену множину диз'юнктів і C - деякий диз'юнкт з MI, такий, що множина MI \ {C} є сумісною. Множина MI є несумісною тоді і тільки тоді, коли в численні lT існує виведення замкненого дерева відносно C з MI в якості вихідної множини.

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

Додавши до lT ще одне правило - правило викреслення ланцюжків CD, ми отримуємо числення lT#, в якому вивідні тільки літеральні дерева з листами, що відрізняються від #.

Правило викреслення ланцюжка CD. Нехай Tr є деяке літеральне дерево і Br - його гілка з листом Lf, що має позначку #. Нехай Ch позначає такий максимальний ланцюжок гілки Br, який, при її перегляді «зверху вниз», закінчується листом Lf і кожен вузол якої, крім з Lf, містить тільки одного спадкоємця. Якщо Tr' позначає результат викреслення з Tr усього ланцюжка Ch, то говориться, що Tr' отримано з Tr за правилом CD.

Щодо числення lT#, має місце такий результат.

Теорема 3.4. Нехай MI позначає скінчену множину диз'юнктів і C - деякий диз'юнкт з MI, такий, що множина MI \ {C} є сумісною. Множина MI є несумісною тоді і тільки тоді, коли в численні lT# існує виведення пустого дерева відносно C з MI в якості вихідної множини.

Наступне поняття зв'язує літеральні дерева з упорядкованими диз'юнктами.

Нехай Tr - непусте дерево пошуку виведення в численні lT#, відмінне від кореня. Його диз'юнктивним образом cl(Tr) є упорядкований диз'юнкт, одержуваний таким чином: якщо L1, ..., Ln - усі літери з листів дерева Tr, перераховані в тому порядку, в якому вони зустрічаються під час перегляду Tr «зверху вниз» і «зліва направо», то cl(Tr) є L1 ... Ln. cl() є .

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

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

Якщо C MI, і C є диз'юнкт L1 ... Ln, то пара <С,i> (1 i n) називається індексом входження літери Lі в C відносно MI. Відзначимо, що при застосуванні будь-яких правил виведення до диз'юнктів з MI, а потім до їхніх наслідків і т. д., зберігаються індекси літер, що належать диз'юнктам з множини MI. Правило слабкої факторизації WF. Нехай C1 L1 C2 ... Cn-1 Ln Cn є диз'юнкт, у якому C1, ..., Cn є диз'юнкти, і L1, ..., Ln є літери, що мають один і той же індекс. Припустимо, що існує н.з.у. множини {L1, ..., Ln}. Тоді кажуть, що з C1 L1 C2 ... Cn-1 Ln Cn за правилом слабкої факторизації WF може бути виведений диз'юнкт (C1 L1 C2 ... Cn)..

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

Вводяться два резолюційних правила: IR и BR. Правило IR являє собою вхідну резолюцію для упорядкованих диз'юнктів, а BR - бінарну резолюцію, яка не застосовується до пари диз'юнктів, коли хоч один із них є вхідним диз'юнктом.

Резолюція в лінійному форматі з правилами WF, IR и BR розуміється в звичайному сенсі.

Використовуючи числення lT#, доводиться її коректність і повнота (теорема 3.5).

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

Таке лінійне виведення з квазіпоглинанням також є коректним і повним резолюційним методом (теорема 3.6)

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

Для дерева пошуку виведення Tr у численні lT# вводиться поняття його модельного диз'юнктивного образу mcl(Tr), що містить усі літери Tr, які упорядковані певним чином при обході дерева справа наліво і знизу вгору, і в яких об'являються обрамленими всі літери, приписані вузлам, які не є листям Tr. За означенням mcl() є .

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

Використовуючи поняття модельного диз'юнктивного образу дерева та повноту числення lT#, доводиться коректність і повнота побудованого метода елімінації моделей.

Теорема 3.7. Нехай D є диз'юнктом із множини вхідних диз'юнктів MI, таким, що множина MI \ {D} є несуперечливою. MI являється суперечливою множиною тоді і тільки тоді, коли існує виведення диз'юнкта відносно D, що задовольняє методу елімінації моделей з правилами MR, RR і LD.

Її наслідком 3.5 є коректність і повнота звичайного методу елімінації моделей Лавленда.

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

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

f(x1, …, xn) = f(x1, …, xn),

де f - функціональний символ, а x1, …, xn - змінні.

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

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

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

Правило бінарної парамодуляції P. Нехай С1 і C2 - упорядковані диз'юнкти (посилки правила), які не мають загальних змінних. Якщо С1 є С1' L[t] С1'', де L[t] - літера, що містить терм t, a С1' і С1'' - деякі диз'юнкти, і якщо C2 є C2' (t' = s) C2'', де C2' і C2'' - деякі диз'юнкти, і s - терм, і при цьому існує н.з.у. множини {t, t`}, то говориться, що з С1 і C2 за правилом бінарної парамодуляції P є вивідним диз'юнкт С1'. L.[s..] С1''. C2'. C2''., де L.[s.] позначає результат заміни одного єдиного входження t. у L. на s... Цей виведений диз'юнкт називається бінарним парамодулянтом диз'юнктів С1 і C2ї. Нижче нам буде зручно говорити, що ми застосовуємо парамодуляцію з диз'юнкта C2 в диз'юнкт С1.

Надалі «напрямки» дії парамодуляції P розрізняються: парамодуляція з вхідного упорядкованого диз'юнкта в будь-який інший буде позначатися Pi, а з будь-якого упорядкованого диз'юнкта у вхідний - Po. Далі, якщо в лінійному виведенні парамодуляція виконується між невхідними диз'юнктами C1 і C2, і C1 передує висновку C2, то парамодуляція із C1 в C2 буде позначатися Pd, а із C2 в C1 - Pu.

Щодо резолюції, то, як і раніше, розглядаються два правила - IR і BR.

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

Теорема 4.1. Нехай MI позначає скінчену множину диз'юнктів, що містить літеру рівності x = x, і C - такий диз'юнкт з MI, що множина MI \ {C} є Е-виконуваною. Множина MI є Е-невиконуваною тоді і тільки тоді, коли існує лінійне виведення диз'юнкта відносно C з MI {x = x} AFR(MI) в якості вихідної множини за допомогою резолюційних правил IR та BR і парамодуляційних правил Pi, Po та Pd (Pi, Po та Pu).

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

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

Правило парамодуляційного розширення Pin. Нехай MI є вихідна множина диз'юнктів, Tr - літеральне дерево і L - мітка найбільш правого листа в Tr, відмінна від #. Припустимо, що MI містить такий диз'юнкт D, що правило парамодуляції P, застосовне в напрямку з С в L, де L розглядається як одиничний диз'юнкт, C - варіант D, і С не має спільних змінних з літерами з Tr. Нехай при цьому застосуванні P породжуються н.о.у. і парамодулянт L1 ... Lk. Тоді кажуть, що дерево, яке є результатом додавання «зліва направо» k спадкоємців L1, ..., Lk до листа L. в дереві Tr., виводиться з Tr за правилом Pin відносно D.

Правило парамодуляційного розширення Pout. Нехай MI є вихідна множина диз'юнктів, Tr - літеральне дерево і L - мітка найбільш правого листа в Tr, відмінна від #. Припустимо, що MI містить такий диз'юнкт D, що правило парамодуляції P застосоване в напрямку з L в C, де L розглядається як одиничний диз'юнкт, C - варіант D, і С не має спільних змінних з літерами з Tr. Нехай при цьому застосуванні P породжуються н.о.у. і парамодулянт L1 ... Lk. Тоді кажуть, що дерево, яке є результатом додавання «зліва направо» k спадкоємців L1, ..., Lk до листа L. в дереві Tr., виводиться з Tr за правилом Pin відносно D.

Правило парамодуляційного розширення Pdown. Нехай MI є вихідна множина диз'юнктів, Tr - літеральне дерево і L - мітка найбільш правого листа в Tr, відмінна від #. Припустимо, що в гілці з листом L існує такий вузол з міткою E, що правило парамодуляції P може бути застосоване з E в L, де E і L розглядаються як одиничні диз'юнкти. Нехай при цьому застосуванні P породжуються н.о.у. і парамодулянт L'. Тоді кажуть, що дерево, яке є результатом додавання одного спадкоємця L' до листа L. в дереві Tr., виводиться з Tr за правилом Pdown відносно E.

Правило парамодуляційного розширення Pup. Нехай MI є вихідна множина диз'юнктів, Tr - літеральне дерево і L - мітка найбільш правого листа в Tr, відмінна від #. Припустимо, що в гілці з листом L існує такий вузол з міткою E, що правило парамодуляції P може бути застосовано з L в E, де E і L розглядаються як одиничні диз'юнкти. Нехай при цьому застосуванні P породжуються н.о.у. і парамодулянт L'. Тоді кажуть, що дерево, яке є результатом додавання одного спадкоємця L' до листа L. в дереві Tr., виводиться з Tr за правилом Pdown відносно E.

Позначимо lT#d (lT#u) числення літеральних дерев, що отримано з lT# додавання до нього правил Pin, Pout і Pdown (Pin, Pout і Pup). Відносно побудованих таким чином числень має місце такий результат (доведення якого базується на теоремі 4.1).

Теорема 4.2. Нехай MI позначає скінчену множину диз'юнктів і C - такий диз'юнкт з MI, що множина MI \ {C} є Е-виконуваною. Множина MI є Е-невиконуваною тоді і тільки тоді, коли в численні lT#d (lT#u) існує виведення пустого дерева відносно C з MI {x = x} AFR(MI) в якості вихідної множини.

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

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

Правило модельної парамодуляції MPi (у вхідний диз'юнкт). Нехай диз'юнкти C1 і C2, які не мають загальних змінних і мають вигляд D1 L і D2 E D'2, де L і E - літери, D1, D2 і D'2 - диз'юнкти (можливо, порожні), причому C2 обов'язково належить MI та існує парамодуляція із L в E з бінарним парамодулянтом E', і при цьому породжується н.з.у. . Тоді кажуть, що із C1 і C2 за правилом модельної парамодуляції MPi може бути виведений диз'юнкт (D1 L D2) . E' D'2 ..

Правило модельної парамодуляції MPo (із вхідного диз'юнкта). Нехай диз'юнкти C1 і C2, які не мають загальних змінних і мають вигляд D1 L і D2 E D'2, де L і E - літери, D1, D2 і D'2 - диз'юнкти (можливо, порожні), причому C2 обов'язково належить MI та існує парамодуляція із E в L з парамодулянтом L', і при цьому породжується н.з.у. . Тоді кажуть, що із C1 і C2 за правилом модельної парамодуляції MPo може бути виведений диз'юнкт D1 . L' (D2 D'2) ..

Правило модельної парамодуляції вліво MPl. Нехай диз'юнкт C має вигляд D1 L D2 E, де L і E - літери, причому L - обрамлена літера, і D1 і D2 - диз'юнкти (можливо, порожні), та існує парамодуляція із E в L з парамодулянтом L' і при цьому породжується н.з.у. . Тоді кажуть, що із C за правилом модельної парамодуляції вліво MPl може бути виведений диз'юнкт (D1 L D2 E ) . L'.

Правило модельної парамодуляції вправо MPr. Нехай диз'юнкт C має вигляд D1 ? D2 E, де L і E - літери, причому L - обрамлена літера, і D1 і D2 - диз'юнкти (можливо, порожні), та існує парамодуляція із E в L з парамодулянтом E' і при цьому породжується н.з.у. . Тоді кажуть, що із C за правилом модельної парамодуляції вправо MPr може бути виведений диз'юнкт (D1 L D2 E) . E '.

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

Теорема 4.3. Нехай MI є множина вхідних диз'юнктів, і C є такий диз'юнкт з MI, що множина MI \ {C} є E-несуперечливою. Множина MI є E-суперечливою тоді і тільки тоді, коли існує виведення пустого диз'юнкту ? з множини MI AFR(MI) {x=x}, і це виведення задовольняє парамодуляційному розширенню метода елімінації моделей, яке містить правила MPi, MPo і MPr (MPi, MPo і MPl). Оскільки при роботі без рівності метод елімінації моделей можна розглядати як повне розширення вхідної резолюції, то теорема 4.3 вказує на «модельний» засіб парамодуляційного розширення вхідної резолюції до повного в загальному випадку методу пошуку виведення в класичної логіці першого порядку з рівністю.

Висновки

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

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

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

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

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

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

Список опублікованих робіт за темою дисертації

Статті у наукових фахових виданнях

1. Про резолюційні стратегії зі слабкою факторизацією. /Афонін А.О. //Вісник Київського університету. Сер.: фіз.-мат. науки. - 2009. - Вип. 4. - C. 69-73.

2. Про спрямовану парамодуляцію в методі елімінації моделей. /Афонін А.О. //Вісник Київського університету. Сер.: фіз.-мат. науки. - 2010. - Вип. 2. - C. 87-91.

3. Про машинно-орієнтовані числення секвенціального типу для класичної логіки першого порядку. /Афонін А.О. //Наукові записки НаУКМА. Сер.: комп. науки. - 2009. - Т. 99. - C. 23-28.

4. О древовидной форме поиска опровержения в интеллектуальных системах с логическими возможностями. /Афонін А.О. //Математичні машини і системи. - 2010. - Вип. 1. - С. 87-95

Тези наукових доповідей

5. Про резолюційні стратегії зі слабкою факторизацією. /Афонін А.О. //Міжнародна конференція «Теоретичні та прикладні аспекти програмних систем». - Київ, 2010. - С. 511-513.

6. О полных расширениях логического апарата Пролог-подобных систем. /Афонін А.О. // Міжнародна конференція «Теоретичні та прикладні аспекти програмних систем». - Київ, 2009. - С. 240-244.

7. Об обработке равенств в линейных стратегиях над упорядоченными дизъюнктами. /Афонін А.О. //XI Міжнародна наукова конференція «Інтелектуальний аналіз інформації». - Київ, 2010. - С.4-9.

8. О резолюционной технике в современных информационных технологиях. /Афонін А.О. //XII Міжнародна конференція «Системний аналіз та інформаційні технології». - Київ, 2010. - С. 198-199.

Анотація

Афонін А.О. Повні методи пошуку виведення в системах логічного програмування. - Рукопис.

Дисертація на здобуття наукового ступеня кандидата фізико-математичних наук за спеціальністю 01.05.01 - теоретичні основи інформатики та кібернетики. - Київський національний університет імені Тараса Шевченка. - Київ, 2011.

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

Класична логіка розглянута як для випадку роботи з рівністю, так і без неї.

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

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

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

Ключові слова: класична логіка першого порядку, секвенційні числення, резолюційний метод, SLD-резолюція, вхідна резолюція, лінійна резолюція, метод елімінації моделей, парамодуляція, коректність, повнота.

Аннотация

Афонин А.А. Полные методы поиска вывода в системах логического программирования. - Рукопись.

Диссертация на соискание ученой степени кандидата физико-математических наук по специальности 01.05.01 - теоретические основы информатики и кибернетики. - Киевский национальный университет имени Тараса Шевченко. - Киев, 2011.

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

В этой связи следует заметить, что достаточно высокая эффективность обработки данных в проблемно-ориентированных интеллектуальных системах обычно достигается за счет того, что их дедуктивный аппарат, как правило, реализует "упрощенную" логическую процедуру, достаточную для решения задач из области, для которой предназначена та или иная система. Поэтому при создании новой системы или оболочки на базе уже имеющейся, которая требует дополнительной логической обработки, можно попытаться просто «дооснастить» ее некоторыми дополнительными дедуктивными механизмами так, чтобы расширить сферу ее применимости на более общий случай, а в идеале, и вообще на случай установления выводимости любых формул. Это с необходимостью приводит к теоретическим исследованиям по корректным и полным расширениям в общем случае тех "упрощенных" методов, которые используются в системах логического программирования.

Возможное решение этого вопроса предлагается в диссертации для случая классической логики первого порядка, как с равенством, так и без него. В ней, главным образом, развиваются исчисления и методы, которые могут рассматриваться как корректные и полные в общем случае расширения дедуктивных возможностей систем логического программирования, где корректность и полнота понимаются в их логическом смысле. Соответствующие теоретические исследования проводятся для классической логики первого порядка, как без равенства, так и с ним.

Для логики без равенства рассмотрен секвенциальный подход к установлению выводимости, который приводит к секвенциальной форме теоремы Эрбрана, не требующей проведения предварительной сколемизации. Это дает основу для получения семейства корректных и полных в общем случае секвенциальных исчислений для поиска вывода в сигнатуре исходной теории. Используя ее, обосновывается полнота целеориентированного исчисления такого типа, которое может быть использовано при построении систем поиска доказательств.

Построены и исследованы на корректность и полноту исчисления литеральных секвенций и литеральных деревьев для случая отсутствия равенства. Установлена связь этих исчислений с предложенными модификациями известных резолюционных методов и стратегий, таких, как SLD-резолюция, входная резолюция, линейная резолюция, метод элиминации моделей. Используя ее, доказана корректность и полнота этих модификаций, что дает возможность проводить корректные и полные расширения дедуктивного аппарата тех интеллектуальных систем, включая системы логического программирования, которые базируются на резолюционной (неполной) технике. Одной из специфик модификаций является то, что они используют упрощение правила факторизации.

Для классической логики с равенством построены парамодуляционные расширения исчисления литеральных деревьев, а также модификаций резолюционных методов и стратегий, включая SLD-резолюцию, входную резолюцию, линейную резолюцию и метод элиминации моделей. Доказана их корректность и полнота в случае использования аксиом функциональной рефлексивности, и показана невозможность получения полноты без этих аксиом.

Диссертация посвящена чисто теоретическим исследованиям. Однако она имеет и практическую направленность, поскольку ее результаты могут служить базисом для построения и расширения логического аппарата не только систем логического программирования, но и других интеллектуальных систем, включая системы автоматизации поиска логического вывода.

Ключевые слова: классическая логика первого порядка, секвенциальное исчисление, резолюционный метод, SLD-резолюция, входная резолюция, линейная резолюция, метод элиминации моделей, парамодуляция, корректность, полнота.

Abstract

Afonin A.O. Complete methods of inference search in logic programming systems. - Manuscript.

The dissertation for a scientific degree of Candidate of Physics and Mathematics on the speciality 01.05.01 - Foundations of Informatics and Cybernetics; Taras Shevchenko National University of Kiev, Kiev, 2011.

The dissertation is devoted to the construction of inference search methods for first-order classical logic and for logic programming systems and their investigation on soundness and completeness.

Classical logic was considered both for formulas with equality and for formulas without it. The following investigations were performed.

For classical logic without equality, a new sequent approach to inference search was constructed, which gave a possibility for proving a sequent form of Herbrand's theorem not requiring preliminary skolemization and, as a result, for the construction of a family of sound and complete sequent-type calculi for inference search in the signature of an initial first-order theory. Using it, the soundness and completeness of a goal-oriented sequent calculus were proven.

In the case of equality absence, calculi of literal sequents and literal trees were constructed. Their connection with given modifications of the well-known resolution methods and strategies, such that the SLD-resolution, input resolution, linear resolution, and model elimination method, was described. Using it, the soundness and completeness of the modification were proven. This permits to build complete extensions of deductive engines of certain intelligent systems, including logic programming systems.

For classical logic with equality, paramodulation extensions of the literal tree calculus and the resolution-type methods and strategies including the SLD-resolution, input resolution, linear resolution, and model elimination method were proved for the case of using functional reflexivity axioms. It was demonstrated that the absence of the axioms can violate completeness.

Key words: first-order classical logic, equality, sequent calculus, resolution-type method, SLD-resolution, input resolution, linear resolution, model elimination method, paramodulation, soundness, completeness.

Размещено на Allbest.ru

...