THE UNIFICATION ALGORITHM FOR THE EXTENSIBLE MODEL OF A MATHEMATICAL DIALECT

In this paper the problem of unification for the extensible model of a mathematical dialect and an algorithm for its solving are considered. It is shown that increasing the level of a language for mathematical knowledge representation used in software for theorems proving leads to a significant complication of the unification algorithm.

Keywords: unification, mathematical statement, propositional statement, meta mathematical statement, semantic variable, propositional variable, syntactic variable, modified syntactic variable.