Search academic texts

Registration Number

0411U005358, Candidate dissertation

Status

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

Date

23-06-2011

popup.evolution

o

Title

Complete methods of inference search in logic programming systems

Author

Afonin Andriu Oleksandrovich,

popup.head Glybovez Mukola Mukolaevich
popup.opponent Клименко Віталій Петрович
popup.opponent Лялецький Олександр Вадимович

Description

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