DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2024.10

Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory

Authors: Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract

We present Duper, a proof-producing theorem prover for Lean based on the superposition calculus. Duper can be called directly as a terminal tactic in interactive Lean proofs, but is also designed with proof reconstruction for a future Lean hammer in mind. In this paper, we describe Duper’s underlying approach to proof search and proof reconstruction with a particular emphasis on the challenges of working in a dependent type theory. We also compare Duper’s performance to Metis' on pre-existing benchmarks to give evidence that Duper is performant enough to be useful for proof reconstruction in a hammer.

Cite as

Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad. Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{clune_et_al:LIPIcs.ITP.2024.10,
  author =	{Clune, Joshua and Qian, Yicheng and Bentkamp, Alexander and Avigad, Jeremy},
  title =	{{Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{10:1--10:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.10},
  URN =		{urn:nbn:de:0030-drops-207381},
  doi =		{10.4230/LIPIcs.ITP.2024.10},
  annote =	{Keywords: proof search, automatic theorem proving, interactive theorem proving, Lean, dependent type theory}
}

Search Results

Documents authored by Clune, Joshua

Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory

Abstract

Cite as

Thanks for your feedback!

Could not send message