Primary tabs

This math archive contains a set of interface theories for aligning common theorem prover libraries. Interface theories contain foundationally unconstrained (and thus abstract) versions of the mathemtatical knowledge. This makes them natural candidates for the MitM ontology.


  • Views:
  • Theories:
  • Definitions:
  • Constants:
  • Files:
  • OMDoc size: K
  • Source size: K
  • Logic.omdoc
  • Math
  • TypeConstructors.omdoc
  • TypeSystem.omdoc