Научный журнал

ISSN 1814-2400

ИНФОРМАТИКА И СИСТЕМЫ УПРАВЛЕНИЯ

Клещев А. С., Тимченко В. А.

Алгоритм унификации для расширяемой модели математического диалекта

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

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