Implementation of the shell and knowledge portal for mathematical proofs verification on the IACPAAS platform

The paper presents a conceptual architecture of the shell for interactive systems for mathematical proofs verification and an evolutionary thematic knowledge portal created with its help. The process of implementation of all software and information components of the shell on the IACPaaS cloud platform with the use of its technologies and tools of their support is described. The process of development of the initial state of the knowledge portal for mathematical proofs verification using shell tools is considered. The way to use the knowledge portal by members of the mathematical community as well as mechanisms for changing the state of the portal by its administrator is discussed. The initial state of the knowledge portal includes: the ontology model of the mathematical knowledge base, including the specification of the initial state of the language for mathematical knowledge representation, the editor for the ontology model of the mathematical knowledge base, the mathematical knowledge base editor, the base of methods of reasoning editor, and the problem solver of the shell that implements the process of constructing proofs in terms of ontology model of proofs. The initial state of the knowledge portal also includes the initial state of the mathematical knowledge base and the initial state of the base of the methods of reasoning. The evolvement of the knowledge portal consists in the development of the three listed information components. All interested members of the mathematical community can participate in this process. It is implemented with the use of personal cabinets of the IACPaaS platform, where each user can independently develop his personal copy of the current state of the common knowledge portal. The transfer of new results to the common knowledge portal is controlled by its administrator.