HackerPapers

arXiv:2508.20738cs.LO

Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL

Lukas Bartl, Jasmin Blanchette, Tobias Nipkow

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

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.

arXiv 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
Journal reference
DOI
doi:10.1007/978-3-031-99984-0_30
Subjects
cs.LOLogic in Computer Science

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Jul 2026 to Jul 2026.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. Are We Stuck with Lean? 1 comment

    • > I think we might now be approaching the situation where I can do my research pretty much as I usually do it, but at the same time in parallel have formalized proofs for the lemmas and theorems. If you were using Isabelle/HOL, then (depending on field) you could already have…

      wizzwizz4View on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.