Пошук академічних текстів

Реєстраційний номер

0411U005358, Кандидатська дисертація

На здобуття

к.ф.-м.н., 01.05.01, Теоретичні основи інформатики та кібернетики

Дата захисту

23-06-2011

Статус

Запланована

Назва роботи

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

Здобувач

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

Керівник Глибовець Микола Миколайович
Опонент Клименко Віталій Петрович
Опонент Лялецький Олександр Вадимович

Опис

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