SUMO to OMDoc/MMT exporter.
The Suggested Upper Merged Ontology SUMO is an upper ontology that lightly formalizes common sense situations. It woucd be very nice to have a translator of SUMO into MMT Theories. For that we need
- A meta-theory for the KIF (Knowledge Interface Format)
- a translator for the SUMO data to OMDoc/MMT. SUMO seems licenced mostly under GPL, so we are allowed to do this and even republish it on MathHub (as long as we keep the GPL).
This would be a good basis for JLogic.