Escape to Mizar for ATPs

TL;DR

This paper introduces a tool that translates derivations from the E theorem prover into Mizar proofs, facilitating interoperability between automated and interactive theorem proving systems.

Contribution

We present a novel tool and methodology for mapping proofs from E to Mizar, addressing challenges in translating between different logical formalizations.

Findings

Successfully mapped E derivations to Mizar proofs

Identified and solved key difficulties in proof translation

Enhanced interoperability between theorem proving systems

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).