Аннотация:
Рассматривается метод поиска вывода в односукцедентном секвенциальном варианте классического исчисления предикатов. В этом алгоритме используются метапеременные и частичная скулемизация. Для рассматриваемого алгоритма доказываются теоремы о корректности и полноте.
Ключевые слова:автоматическое доказательство теорем, поиск вывода, язык первого порядка, исчисление предикатов, исчисление секвенций, продукционная система, искусственный интеллект.
Полный текст:
PDF файл (551 kB)