Integrate Theorem provers into MMT
OMDoc/MMT allows to represent a wide range of logics and reasoning calculi as (meta)-theories via the Curry/Howard isomoprphism. The MMT system supplies automated type- and this proof-checking for all of these out of the box. But it does not offer any proof automation.
For some logics - e.g. first-order logic - we have very good proof automation - e.g. EProver, Spass, Vampire, the Hammers, ... So we could get proof automation in MMT by just translating to the input language of these and when they can find a proof obtain back a proof certificicate (translating that into the existing ND calculus we can leave to a later stage).
- This idea should be implemented in MMT for one instance (e.g. FOLEQ and EProver) so that we can increase proof efficiency (and proofs are the most important check of adequacy of formalizations).
- Building on this, we want to develop a general infrastructure for more logics and provers
- Finally, we should extend this to even more logics by using views induced by conservative extensions. These translate "super-logics" back down to the "source logics". If there is a prover for the "source logic", then we can use it in the "super-logic".
This would one of the most important extensions of the OMDoc/MMT ecosystem. @dmueller @frabe
To upload designs, you'll need to enable LFS. More information