Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic
En palabras de los autores
We identify common challenges and requirements for verifying proofs from automated theorem provers in the Dedukti logical framework and develop a general methodology for deriving encodings of calculus rules and proof steps, including clausification. We then apply this methodology to the EP calculus for higher-order logic and integrate it into the automated theorem prover Leo-III. The resulting prototype reconstructs about 80% of generated proof steps automatically, making Leo-III the first higher-order automated theorem prover to support independently checkable proof reconstruction and providing a basis for cross-system reuse. The implementation uncovered several bugs in Leo-III.
Apareció: martes, 22 de septiembre. arXiv. Preprint con versión publicada.
Versión publicada: LPAR-26 - 26th Conference on Logic for Programming, Artificial intelligence, and Reasoning, Oct 2026, Spetses Island, Greece