Lukas Bartl
Research Subjects
Lukas Bartl has a total of 2 co-authors. Here are the top co-authors by number of shared publications:
- Jasmin Blanchette
Ludwig-Maximilians-Universität München
1 shared publication - Tobias Nipkow
Technical University of Munich
1 shared publication
Latest Publications
- Open Access
- 30 July 2025
- Published by Springer Nature
- p. 573-593
Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
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.
- 30 July 2025
- Published by Springer Nature
- p. 573-593
Open AccessExploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
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.