Scientific journal

ISSN 1814-2400

INFORMATION SCIENCE AND CONTROL SYSTEMS

Kleschev A. S., Timchenko V. A.

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.