Метод подъема решений для работы с метапеременными в системе TH$\exists$OREM$\forall$

Данная работа посвящена применению метода метапеременных для поиска доказательств в исчислениях секвенциального вида. Описывается эффективный способ работы с метапеременными и его реализация в системе TH$\exists$OREM$\forall$. В основе метода лежит специальная техника работы с метапеременными для случая, когда алгоритм поиска доказательств представляется в виде AND/OR-дерева. Реализация метода не зависит от стратегии поиска и легко интегрируется с другими специализированными методами поиска доказательств, а также со специальными процедурами унификации и поиска решений. Мы демонстрируем работу метода в контексте специализированной стратегии поиска, применяемой для задач элементарного математического анализа. Библ. – 28 назв.