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

 Автореферати дисертацій 

---

Додаткова інформація про автора(ів) публікації:
(cписок формується автоматично, до списку можуть бути включені персоналії з подібними іменами або однофамільці)

• Афонін Андрій Олександрович (фізико-математичні науки)

  Якщо, ви не знайшли інформацію про автора(ів) публікації, маєте бажання виправити або відобразити більш докладну інформацію про науковців України запрошуємо заповнити "Анкету науковця"