I would like to know if there are any proof formats which is used to exchange proofs among proof assistants. I realize different proof assistants use different foundations but for those that have the same or similar foundations are there any standard formats?
5
-
1$\begingroup$ jesper.sikanda.be/files/AIMXXXI-presentation.pdf I'll let qualified people give a more substantial answer. $\endgroup$– Li-yao XiaJan 4 at 11:31
-
1$\begingroup$ Here's a related question: Is there a way to automatically translate proofs from one proof assistant to another? $\endgroup$– ChesiumJan 4 at 13:41
-
$\begingroup$ This is also related: Does there exists a logical format so that my app can export in that format, and the existing popular proof assistants can take it as input? $\endgroup$– Jason RuteJan 4 at 19:54
-
$\begingroup$ @jude Do either of these two linked questions answer your question? If so we can mark it as a duplicate. $\endgroup$– Jason RuteJan 6 at 17:15
-
$\begingroup$ @JasonRute They were informative and enough for my needs so I dont mind it being marked as duplicate. But imho i dont think they are definitive enough (if at all there is a definitive answer). $\endgroup$– judeJan 7 at 18:18
Add a comment
|
3 Answers
$\begingroup$
$\endgroup$
The OpenTheory system has a standard format for the core HOL logics supported by HOL Light, HOL4, ProofPower and HOL Zero.
$\begingroup$
$\endgroup$
There is also the TPTP format for theorem prover problems. It acts as a pretty standard format for stating results in a "prover independent" manner.
