Задача применения подстановки для расширяемой модели математического диалекта
Рассмотрена задача применения подстановки для расширяемой модели математического диалекта и приведен алгоритм ее решения. Показано, что повышение уровня языка представления математических знаний, используемого в системах компьютерного доказательства теорем, ведет к заметному усложнению алгоритма применения подстановки.
Ключевые слова: подстановка, математическое утверждение, пропозициональное утверждение, метаматематическое утверждение, предметная переменная, пропозициональная переменная, синтаксическая переменная, модифицированная синтаксическая переменная.
