Побудова методів пошуку виведення в класичній логіці першого порядку. Дослідження систем логічного програмування на коректність і повноту. Модуляційні розширення числення літеральний дерев. Модифікація резолюційних стратегій і методу елімінації моделей.
Аннотация к работе
КИЇВСЬКИЙ НАЦІОНАЛЬНИЙ УНІВЕРСИТЕТ Автореферат дисертації на здобуття вченого ступеня кандидата фізико-математичних наукНауковий керівник: доктор фізико-математичних наук, професор Глибовець Микола Миколайович, Національний університет «Києво-Могилянська академія», декан факультету інформатики Офіційні опоненти: доктор фізико-математичних наук, професор Клименко Віталій Петрович, Інститут проблем математичних машин і систем НАН України, м.Київ, заступник директора з наукової роботи кандидат фізико-математичних наук, с.н.с. Захист дисертації відбудеться «23» червня 2011 р. о 14 годині на засіданні спеціалізованої вченої ради Д 26.001.09 Київського національного університету імені Тараса Шевченка за адресою: 03680, м.Це насамперед стосується аспектів пошуку виведення в класичній логіці першого порядку, що дали широкий спектр засобів проведення дедуктивних побудов в інтелектуальних системах, зокрема в системах логічного програмування, які, як правило, використовують неповні методи, але які можна спробувати застосувати для вирішення більш різноманітних логічних завдань, наприклад, просто в якості систем автоматизації доведень. Побудувати та теоретично дослідити методи і числення пошуку виведення в класичній логіці першого порядку, які можуть розглядатися як повні розширення добре відомої логічної техніки, що зазвичай використовується в системах логічного програмування. Методи дослідження базуються на підходах до досліджень з автоматизації міркувань у формальних теоріях, а також на результатах математичної і компютерної логік, теорії побудов систем логічного програмування. Наукове значення роботи полягає в тому, що, по-перше, побудовано та теоретично досліджено на коректність і повноту нові компютерно-орієнтовані методи пошуку логічного виведення в класичній логіці першого порядку, і, по-друге, досліджено можливість побудови на базі цих методів повних розширень логічного апарату систем логічного програмування зокрема та інтелектуальних систем взагалі, враховуючи випадок роботи з рівністю. Незважаючи на те, що дисертація має теоретичну спрямованість, про її практичне значення говорить те, що отримані результати можуть бути застосовані в загальній теорії побудови інтелектуальних систем із логічними можливостями, для розширення дедуктивних можливостей систем логічного програмування, а також для побудови повних систем автоматичного пошуку виведення в класичній логіці першого порядку (з рівністю і без неї).Розвинено новий секвенційний підхід до побудови машинно-орієнтованих числень, які не вимагають проведення попередньої сколемізації, що дозволяє довести секвенціальний варіант теореми Ербрана, який використовує оригінальне поняття допустимої підстановки й веде до побудови нових секвенціальних методів пошуку виведення, не потребуючих проведення сколемізації. Побудовано і досліджено на коректність і повноту машинно-орієнтовані числення секвенціального типу, що не потребують проведення сколемізації. Зокрема, побудовано і досліджено на коректність і повноту так зване числення літеральних дерев.
Вывод
Основним результатом дисертації є розроблення та вивчення нових методів секвенціального і резолюційного типів пошуку виведення в класичній логіці першого порядку (як з рівністю, так і без неї). В ній виконано такі теоретичні дослідження: 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.