Registration Number
0411U005358, Candidate dissertation
Status
к.ф.-м.н.
Date
23-06-2011
popup.evolution
.
Title
Complete methods of inference search in logic programming systems
Author
Afonin Andriu Oleksandrovich,
popup.head Glybovez Mukola Mukolaevich
popup.opponent Клименко Віталій Петрович
popup.opponent Лялецький Олександр Вадимович
popup.rada
Taras Shevchenko Kiev University
Description
Дисертацію присвячено побудові методів пошуку виведення в класичній логіці першого порядку, які можуть бути використані в системах логічного програмування, та їх теоретичному дослідженню на коректність і повноту, де коректність і повнота розуміються в логічному сенсі. Класична логіка розглянута як для випадку роботи з рівністю, так і без неї. Для логіки без рівності розроблено секвенційний підхід до встановлення вивідності, що дав змогу довести секвенційну форму теореми Ербрана, яка не потребує проведення попередньої сколемізації. Це дає основу для побудови сімейства коректних і повних, в загальному випадку, числень секвеційного типу для пошуку виведення в сигнатурі вихідної теорії першого порядку. Використовуючи її, доводиться повнота цілеорієнтованого числення такого типу.
Registration Date
2011-07-14
popup.nrat_date
2020-04-04 / 2026-06-30
