|
Description
|
Theory morphisms are ubiquitous in mathematics and lie at the heart of the broad applicability of many mathematical theorems. This project aims at harnessing theory-morphisms for mathematicians' daily work by explicitly storing the links between theories and exploiting the resulting graph structure. Storage and retrieval of theories and their morphisms is done using OMDoc's Complex Theories and Development Graphs modules. This implementation offers a variety of value services, e.g., searching in the presence of theory morphisms which builds upon the MathWebSearch search engine, or shallow proof assistance.
|