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

  Скачати повний текст

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

  Скачати повний текст