4
$\begingroup$

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?

$\endgroup$
5

3 Answers 3

2
$\begingroup$

The OpenTheory system has a standard format for the core HOL logics supported by HOL Light, HOL4, ProofPower and HOL Zero.

$\endgroup$
1
$\begingroup$

There's also Metamath Zero by Mario Carneiro

$\endgroup$
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.