Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
Logic in Computer Science
2025-08-29 v1
Abstract
Metis is an ordered paramodulation prover built into the Isabelle/HOL proof assistant. It attempts to close the current goal using a given list of lemmas. Typically these lemmas are found by Sledgehammer, a tool that integrates external automatic provers. We present a new tool that analyzes successful Metis proofs to derive variable instantiations. These increase Sledgehammer's success rate, improve the speed of Sledgehammer-generated proofs, and help users understand why a goal follows from the lemmas.
Cite
@article{arxiv.2508.20738,
title = {Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL},
author = {Lukas Bartl and Jasmin Blanchette and Tobias Nipkow},
journal= {arXiv preprint arXiv:2508.20738},
year = {2025}
}
Comments
This version of the contribution has been accepted for publication in CADE-30, after peer review but is not the Version of Record and does not reflect post-acceptance improvements, or any corrections