Theoretical foundations for creation of a shell for interactive systems of intuitive mathematical proofs’ verification

The article presents a concept of a shell for interactive systems of intuitive mathematical proofs. The means of specifying formal systems that can be used as theoretical foundations for this shell are considered: the languages for description of generative graph and text grammars, as well as the language for context conditions description. These languages allow defining context-dependent graph grammars with a specific syntax. With the use of these means, the kernel of a formal logical system that is connected to the mathematical practice of proofs’ constructing is specified. The model of ontology for representation of the bases of formalized mathematical knowledge and methods of reasoning is described. This model includes the specification of the network structure of various sections of mathematics, as well as the specification of generative graph grammars describing the abstract syntax of the languages for mathematical statements (knowledge) and methods of reasoning representation. The context conditions of these languages are also defined. The common syntactic structure of proofs and the model of ontology of proofs, developed on its basis, are considered. We apply the approach based on context-dependent grammars and ontologies. It consists in the development of an explicitly presented declarative specification of the language for mathematical knowledge and methods of reasoning (the language of a mathematical dialect) representation, as well as a model of proof. The key feature of the language is its extensibility, which is provided by the extensibility of a set of definitions that allow us to introduce new terms to denote the defined concepts and the extensibility of its grammar. The extensibility of grammar is achieved thanks to the means that allow one to describe the syntax of each new construction of the language for mathematical statements’ representation, as well as the context conditions.