Аннотация:
Статья является продолжением статьи [1]. Рассматривается алгоритм верификации формализованных математических доказательств для логики предикатов первого порядка с равенством. Доказываются теоремы о его корректности и полноте.
Ключевые слова:автоматическое доказательство теорем, система автоматизации дедукции, верификация доказательств, язык первого порядка, исчисление предикатов, продукционная система, искусственный интеллект.
Полный текст:
PDF файл (370 kB)