Abstract
The problem of the integrity of a computer managed mathematical knowledge repository is in the heart of MKM since mathematical vernacular is a language permitting plenty of ways in expressing the same meaning. The users of the library are naturally forced to choose certain way among many similar ones, unless different approaches are provided by developers. Mizar is a system for formalizing mathematical content which is sufficient mature and flexible for a coexistence of different approaches of concrete subjects. Considering Mizar formalizations of ortholattice theory we discuss a useful mechanism of coping with the heterogeneity of theories in a library of mathematical facts. © Springer-Verlag Berlin Heidelberg 2004.
Cite
CITATION STYLE
Grabowski, A., & Moschner, M. (2004). Managing heterogeneous theories within a mathematical knowledge repository. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3119, 116–129. https://doi.org/10.1007/978-3-540-27818-4_9
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
