Elamur Research⌕
☰
home / papers / 2024 / Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory

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

Paper · 2024 · Joshua Clune, Yicheng Qian, Alexander Bentkamp et al.

Summary

Lean has no hammer, i.e. a tool that sends goals to external automatic provers and then rebuilds checkable proofs from their output. Building one for a dependently typed foundation is difficult. The authors present Duper, a superposition-based prover written in Lean that outputs proof terms directly in Lean's axiomatic foundation. Users can call it as a terminal tactic, and it is also intended as the proof-reconstruction component of a future Lean hammer. Proof search runs a saturation loop that adapts Zipperposition's higher-order techniques. Dependent-type issues are handled in two ways. Some are delegated to the LeanAuto preprocessing tool, such as type class instantiation and monomorphization. Others are treated natively, such as Skolemization when a quantifier may range over an empty type, and polymorphism over types and universes. The authors evaluated Duper against Metis on the Seventeen provers and GRUNGE benchmarks. Metis is slightly ahead on raw TPTP problems, but the two are nearly equal on problems already minimized by stronger external provers. This suggests Duper is fast enough for hammer-style reconstruction.

Key points

  • Duper is based on Zipperposition's oλSup calculus and uses a higher-order extension of the Knuth-Bendix order (KBO). Its main loop is a DISCOUNT-loop variant designed by Vukmirović et al.
  • The implementation keeps two forms of each clause: permanent clauses and modifiable "mclauses", which represent variables as Lean metavariables during unification.
  • On TPTP, no FOF problem needed Duper's expensive rules, while 46 THF problems did. These rules are mostly higher-order.
  • Unlike Metis, Duper reasons natively in higher-order logic. For example, it proves a Finset.sum_add_distrib summation goal that Metis cannot reconstruct after translating it to first-order logic.
  • Current limitation: Duper has no relevance filter, so users must supply lemmas by hand, and no Mathlib-based evaluation was possible. The code is at github.com/leanprover-community/duper.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Carnegie Mellon UniversityPittsburgh · United States633 works · 195,218 citations🎓Peking UniversityBeijing · China335 works · 43,758 citations🎓Heinrich Heine University DüsseldorfDüsseldorf · Germany36 works · 1,654 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Joshua Clune, Yicheng Qian, Alexander Bentkamp and Jeremy Avigad. 2024. Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory. ITP 2024 (LIPIcs 309).

The paper itself, not this page. BibTeX from the library's record of the work.

@inproceedings{clune2024duper,
  title = {{Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory}},
  author = {Joshua Clune, Yicheng Qian, Alexander Bentkamp and Jeremy Avigad},
  booktitle = {ITP 2024 (LIPIcs 309)},
  year = {2024},
  doi = {10.4230/lipics.itp.2024.10},
  url = {https://doi.org/10.4230/lipics.itp.2024.10}
}

References

21 references, 2 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Jürgen Avenhaus, Jörg Denzinger, and Matthias Fuchs. DISCOUNT: A system for distributed equational deduction. In Jieh Hsiang, editor, Rewriting Techniques and Applications, 6th International Conference, RTA-95, Kaiserslautern, Germany, April 5-7, 1995, Proceedings, volume 914 of Lecture Notes in Com… find
  2. Springer, 1995. doi: 10.1007/3-540-59200-8_72. Jeremy Avigad, Leonardo de Moura, Soonho Kong, and Sebastian Ullrich. Theorem proving in Lean 4. URL: https://leanprover.github.io/theorem_proving_in_lean4/. Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and… ↗
  3. An EATCS Series. Springer, 2004. doi:10.1007/978-3-662-07964-5. Jasmin Blanchette, Qi Qiu, and Sophie Tourret. Verified given clause procedures. In Brigitte Pientka and Cesare Tinelli, editors, Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-… — [doi:10.1007/978-3-662-07964-5](https://doi.org/10.1007/978-3-662-07964-5) find
  4. Springer, 2023. doi:10.1007/978-3-031-38499-8_4. Jasmin C. Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. Hammering towards QED. J. Formaliz. Reason., 9(1):101–148, 2016. doi:10.6092/ISSN.1972-5787/4593. Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of Agda – A functio… — [doi:10.1007/978-3-031-38499-8_4](https://doi.org/10.1007/978-3-031-38499-8_4) find
  5. Springer, 2009. doi:10.1007/978-3-642-03359-9_6. Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, and Josef Urban. GRUNGE: A grand unified ATP challenge. In Pascal Fontaine, editor, Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil… — [doi:10.1007/978-3-642-03359-9_6](https://doi.org/10.1007/978-3-642-03359-9_6) find
  6. Springer, 2019. doi:10.1007/978-3-030-29436-6_8. Mario Carneiro, Chad E. Brown, and Josef Urban. Automated theorem proving for metamath. In Adam Naumowicz and René Thiemann, editors, 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland,… — [doi:10.1007/978-3-030-29436-6_8](https://doi.org/10.1007/978-3-030-29436-6_8) find
  7. Springer, 2020. doi:10.1007/978-3-030-51054-1_3. Lukasz Czajka and Cezary Kaliszyk. Hammer for coq: Automation for dependent type theory. J. Autom. Reason., 61(1-4):423–453, 2018. doi:10.1007/S10817-018-9458-4. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming langua… find
  8. Springer, 2021. doi:10.1007/978-3-030-79876-5_37. Martin Desharnais, Petar Vukmirovic, Jasmin Blanchette, and Makarius Wenzel. Seventeen provers under the hammer. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 20… find
  9. Springer, 2011. doi:10.1007/978-3-642-20398-5_10. Benjamin Grégoire and Assia Mahboubi. Proving equalities in a commutative ring done right in Coq. In Joe Hurd and Thomas F. Melham, editors, Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25,… — [doi:10.1007/978-3-642-20398-5_10](https://doi.org/10.1007/978-3-642-20398-5_10) find
  10. Springer, 2005. doi:10.1007/11541868_7. John Harrison. Optimizing proof search in model elimination. In Michael A. McRobbie and John K. Slaney, editors, Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings,… — [doi:10.1007/11541868_7](https://doi.org/10.1007/11541868_7) find
  11. Springer, 1996. doi: 10.1007/3-540-61511-3_97. Joe Hurd. First-order proof tactics in higher-order logic theorem provers. In Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), pages 56–68, 2003. URL: http://www.gilith.com/papers. Cezary Kaliszyk and Josef Urban. Hol(y… — [doi:10.1007/3-540-61511-3_97](https://doi.org/10.1007/3-540-61511-3_97) ↗
  12. Pergamon, 1970. doi:10.1016/b978-0-08-012975-4.50028-x. Laura Kovács and Andrei Voronkov. First-order theorem proving and vampire. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Procee… find
  13. Springer, 2013. doi:10.1007/ 978-3-642-39799-8_1. Jannis Limperg and Asta Halkjær From. Aesop: White-box best-first proof search for lean. In Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, and Steve Zdancewic, editors, Proceedings of the 12th ACM SIGPLAN International Conference on Certified P… find
  14. Bernd Löchner. Things to know when implementing KBO. J. Autom. Reason., 36(4):289–310, 2006. doi:10.1007/S10817-006-9031-4. Ewing L. Lusk. Controlling redundancy in large search spaces: Argonne-style theorem proving through the years. In Andrei Voronkov, editor, Logic Programming and Automated Reaso… — [doi:10.1007/s10817-006-9031-4](https://doi.org/10.1007/s10817-006-9031-4) find
  15. Springer, 1992. doi:10.1007/BFB0013052. The mathlib Community. The Lean mathematical library. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 367… — [doi:10.1007/bfb0013052](https://doi.org/10.1007/bfb0013052)
  16. ACM, 2020. doi:10.1145/3372885.3373824. William McCune and Larry Wos. Otter–the CADE-13 competition incarnations. Journal of Automated Reasoning, 18(2):211–220, 1997. doi:10.1023/a:1005843632307. Jia Meng and Lawrence C. Paulson. Translating higher-order clauses to first-order clauses. J. Autom. Rea…
  17. EasyChair, 2010. doi:10.29007/36DT. Lawrence C. Paulson and Kong Woei Susanto. Source-level proof reconstruction for interactive theorem proving. In Klaus Schneider and Jens Brandt, editors, Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany,… — [doi:10.29007/36dt](https://doi.org/10.29007/36dt) find
  18. Springer, 2007. doi:10.1007/978-3-540-74591-4_18. William W. Pugh. The test: a fast and practical integer programming algorithm for dependence analysis. In Joanne L. Martin, editor, Proceedings Supercomputing ’91, Albuquerque, NM, USA, November 18-22, 1991, pages 4–13. — [doi:10.1007/978-3-540-74591-4_18](https://doi.org/10.1007/978-3-540-74591-4_18) find
  19. ACM, 1991. doi:10.1145/125826.125848. Konrad Slind and Michael Norrish. A brief overview of HOL4. In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings,… find
  20. Springer, 2008. doi: 10.1007/978-3-540-71067-7_6. Robert Solovay, R. D. Arthan, and John Harrison. Some new results on decidability for elementary algebra and geometry. Ann. Pure Appl. Log., 163(12):1765–1802, 2012. doi: 10.1016/J.APAL.2012.04.003. G. Sutcliffe. The CADE-27 Automated Theorem Proving… — [doi:10.1007/978-3-540-71067-7_6](https://doi.org/10.1007/978-3-540-71067-7_6) find
  21. Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret. Making Higher-Order Superposition Work, pages 415–432. Springer International Publishing, 2021. doi:10.1007/978-3-030-79876-5_24. Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin. Effici… — [doi:10.1007/978-3-030-79876-5_24](https://doi.org/10.1007/978-3-030-79876-5_24) find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/clune-2024-duper-proof-producing-superposition-theorem/