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

  Завантажити