MathHub Interoperability
MathHub.info serves three main purposes:
- to conserve the legacy of the semi-formal material produced by the academic community and protect it from eventualities like disk crashes or the retirement of professors.
- to act as a neutral meeting ground for researchers and clearing house, where the state of the art in FlexiForms can be evaluated and individual results can be compared.
- to act as a repository for reusable specification components like axiomatizations, theorems, and proofs that can serve as the shoulders of giants for individual researchers who reach for the stars.
To reach all of these, we need to make the FlexiForms interoperable and interchangeable, otherwise comparability (2) and reuse (3) is lost and archiving becomes pointless, if we cannot read the conserved resources (1). To obtain interoperability, MathHub standardizes the FlexiForms to the ​OMDoc format. In MathHub OMDoc acts as a theory-neutral representation format that allows to represent the meta-theoretic foundations of the FlexiForms in the same format and to interlink the foundations at the meta-logical level. The OMDoc format incorporates a module system geared to support flexible reuse of specification components via theory morphisms and views. In particular, the logical foundations of domain representations in FlexiForms can be represented as modules themselves and can be interlinked via meta-morphisms. This allows to make FlexiForms interoperable at multiple levels.