Implementation of Type Theory as a Tool for Perceiving Mathematical Theory in Developed Software
Abstract
One of the most important tools for understanding the world around us and applying modern high-tech methods is the mathematical apparatus. Modern mathematical research requires strict formalism and systematization of knowledge, which is especially relevant in the context of developing areas in mathematics. One of the ways to present our perception as a classification of objects and events in terms of types in the sense of TTR (type theory with records) is used in this work. This approach is more flexible and allows the process to be accompanied by visualization through graphs.
The work describes and designs types, defines their relationships and dependencies, which made it possible to organize a clear hierarchy of data. Using the proposed types, a database of mathematical knowledge was created, which is presented in the form of atomic, linear and systematizing notes. For its implementation, Obsidian applications and HTML, Markdown and TeX markup languages combination with the CSS style language were used.
Additionally, a web application was developed to work with this database. The application is written in PHP using a modular architecture, implemented without the use of template engines, and ParseDown was used to parse Markdown into HTML. The backend of the application is built using the MVC architecture. The frontend uses a modular architecture (Dist modules) and a component approach, which improves the extensibility of the system. This development can be used for educational and research purposes, as well as for the creation and systematization of mathematical data in various fields of science.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Publication policy of the journal is based on traditional ethical principles of the Russian scientific periodicals and is built in terms of ethical norms of editors and publishers work stated in Code of Conduct and Best Practice Guidelines for Journal Editors and Code of Conduct for Journal Publishers, developed by the Committee on Publication Ethics (COPE). In the course of publishing editorial board of the journal is led by international rules for copyright protection, statutory regulations of the Russian Federation as well as international standards of publishing.
Authors publishing articles in this journal agree to the following: They retain copyright and grant the journal right of first publication of the work, which is automatically licensed under the Creative Commons Attribution License (CC BY license). Users can use, reuse and build upon the material published in this journal provided that such uses are fully attributed.
