@inproceedings{1f424584e7ee4ff8a4c5c785c566f0bd,
title = "Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL",
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{\textquoteright}s success rate, improve the speed of Sledgehammer-generated proofs, and help users understand why a goal follows from the lemmas.",
keywords = "Isabelle/HOL, Sledgehammer, instantiations, paramodulation",
author = "Lukas Bartl and Jasmin Blanchette and Tobias Nipkow",
note = "Publisher Copyright: {\textcopyright} The Author(s) 2025.; 30th International Conference on Automated Deduction, CADE 2025 ; Conference date: 28-07-2025 Through 31-07-2025",
year = "2025",
doi = "10.1007/978-3-031-99984-0\_30",
language = "English",
isbn = "9783031999833",
series = "Lecture Notes in Computer Science",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "573--593",
editor = "Clark Barrett and Uwe Waldmann",
booktitle = "Automated Deduction - CADE 30 - 30th International Conference on Automated Deduction, 2025, Proceedings",
}