# Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL

## TL;DR

This paper introduces a new tool that analyzes Metis proofs in Isabelle/HOL to derive variable instantiations, enhancing proof automation, speed, and user understanding.

## Contribution

The novel tool automatically extracts variable instantiations from Metis proofs, improving Sledgehammer's effectiveness and proof transparency in Isabelle/HOL.

## Key findings

- Increases Sledgehammer's success rate
- Speeds up proof generation
- Aids user understanding of proof steps

## 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.