Escape to Mizar for ATPs

Abstract

We announce a tool for mapping derivations of the E theorem prover to Mizar proofs. Our mapping complements earlier work that generates problems for automated theorem provers from Mizar inference checking problems. We describe the tool, explain the mapping, and show how we solved some of the difficulties that arise in mapping proofs between different logical formalisms, even when they are based on the same notion of logical consequence, as Mizar and E are (namely, first-order classical logic with identity).

10 pages. Submitted to PAAR 2012 (Practical Aspects of Automated Reasoning, Manchester, June 2012, http://www.eprover.org/EVENTS/PAAR-2012.html)