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