Модель аналогии между математическими доказательствами

На основе расширяемой модели математической практики построена модель аналогии между доказательствами. Исходное доказательство обобщается путем замены некоторых его частей глобальными синтаксическими переменными; целевое доказательство получается из обобщения как результат применения к нему синтаксической подстановки вместо глобальных синтаксических переменных. Задачи обнаружения аналогии, построения целевого доказательства по аналогии, генерации лемм, необходимых для построения целевого доказательства по аналогии, а также генерации теорем, аналогичных исходной, состоят в поиске такой синтаксической подстановки.