Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
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)
@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} }
Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin. Efficient Full Higher-Order Unification. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{vukmirovic_et_al:LIPIcs.FSCD.2020.5, author = {Vukmirovi\'{c}, Petar and Bentkamp, Alexander and Nummelin, Visa}, title = {{Efficient Full Higher-Order Unification}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {5:1--5:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.5}, URN = {urn:nbn:de:0030-drops-123271}, doi = {10.4230/LIPIcs.FSCD.2020.5}, annote = {Keywords: unification, higher-order logic, theorem proving, term rewriting, indexing data structures} }
Feedback for Dagstuhl Publishing