Scholarlink

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.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL

  • 会议论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年

查看全文
  • Lukas Bartl,
  • Jasmin Blanchette,
  • Tobias Nipkow

摘要

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.