THE PROBLEM OF SUBSTITUTION FOR THE EXTENSIBLE MODEL OF A MATHEMATICAL DIALECT
In this paper the problem of application of substitution 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 algorithm for application of substitution.
Keywords: substitution, mathematical statement, propositional statement, meta mathematical statement, semantic variable, propositional variable, syntactic variable, modified syntactic variable.
