Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912557819756544 |
|---|---|
| author | Bartl, Lukas Blanchette, Jasmin Nipkow, Tobias |
| author_facet | Bartl, Lukas Blanchette, Jasmin Nipkow, Tobias |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_20738 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL Bartl, Lukas Blanchette, Jasmin Nipkow, Tobias Logic in Computer Science 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. |
| title | Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2508.20738 |