Внутренняя модель математической практики для систем автоматизированного конструирования доказательств теорем. Ч. 1. Общее описание модели

Для разработки автоматизированных систем конструирования правильных доказательств математических утверждений на основе математических знаний предложена модель математической практики, более адекватная, чем модели математической логики. Модель математической практики представлена в виде комбинации двух моделей: внутренней модели – формальной системы, и внешней модели, в рамках которой математик управляет процессом конструирования интуитивных доказательств. Сформулированы требования к внешней и внутренней моделям математической практики. Дано общее описание внутренней модели.