Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL

Lukas Bartl, Jasmin Blanchette and Tobias Nipkow

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.

pdf

BibTeX:

@inproceedings{KreuzerN-CADE23,
author={Lukas Bartl and Jasmin Blanchette and Tobias Nipkow},
title={Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL},
booktitle="Automated Deduction --- CADE-30",editor={C. Barrett and U. Waldmann},
year=2025,publisher={Springer},series={LNCS},volume={15943},pages={573--593}}