Document Open Access Logo

Efficient Full Higher-Order Unification

Authors Petar Vukmirović , Alexander Bentkamp , Visa Nummelin

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.5.pdf
  • Filesize: 0.54 MB
  • 17 pages

Document Identifiers

Author Details

Petar Vukmirović
  • Vrije Universiteit Amsterdam, The Netherlands
Alexander Bentkamp
  • Vrije Universiteit Amsterdam, The Netherlands
Visa Nummelin
  • Vrije Universiteit Amsterdam, The Netherlands

Funding

Vukmirović and Bentkamp’s research has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Nummelin has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).

Acknowledgements

We are grateful to the maintainers of StarExec for letting us use their service. We thank Ahmed Bhayat, Jasmin Blanchette, Daniel El Ouraoui, Mathias Fleury, Pascal Fontaine, Predrag Janičić, Robert Lewis, Femke van Raamsdonk, Hans-Jörg Schurr, Sophie Tourret, Dmitriy Traytel, and the anonymous reviewers for suggesting many improvements to this text.

Cite AsGet BibTex

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)
https://doi.org/10.4230/LIPIcs.FSCD.2020.5

Abstract

We developed a procedure to enumerate complete sets of higher-order unifiers based on work by Jensen and Pietrzykowski. Our procedure removes many redundant unifiers by carefully restricting the search space and tightly integrating decision procedures for fragments that admit a finite complete set of unifiers. We identify a new such fragment and describe a procedure for computing its unifiers. Our unification procedure is implemented in the Zipperposition theorem prover. Experimental evaluation shows a clear advantage over Jensen and Pietrzykowski’s procedure.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Theorem proving algorithms
Keywords
  • unification
  • higher-order logic
  • theorem proving
  • term rewriting
  • indexing data structures

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann. Superposition with lambdas. In Pascal Fontaine, editor, CADE-27, volume 11716 of LNCS, pages 55-73. Springer, 2019. Google Scholar
  2. Ahmed Bhayat and Giles Reger. Restricted combinatory unification. In Pascal Fontaine, editor, CADE-27, volume 11716 of LNCS, pages 74-93. Springer, 2019. Google Scholar
  3. Chad E. Brown. Satallax: An automatic higher-order prover. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, IJCAR 2012, volume 7364 of LNCS, pages 111-117. Springer, 2012. Google Scholar
  4. Nicolaas G. De Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. J. Symb. Log., 40(3):470-470, 1975. Google Scholar
  5. Simon Cruanes. Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond. PhD thesis, École polytechnique, 2015. Google Scholar
  6. Simon Cruanes. Superposition with structural induction. In Clare Dixon and Marcelo Finger, editors, FroCoS 2017, volume 10483 of LNCS, pages 172-188. Springer, 2017. Google Scholar
  7. Daniel J. Dougherty. Higher-order unification via combinators. Theor. Comput. Sci., 114(2):273-298, 1993. Google Scholar
  8. William M. Farmer. A unification algorithm for second-order monadic terms. Ann. Pure Appl. Logic, 39(2):131-174, 1988. Google Scholar
  9. Krystof Hoder and Andrei Voronkov. Comparing unification algorithms in first-order theorem proving. In Bärbel Mertsching, Marcus Hund, and Muhammad Zaheer Aziz, editors, KI 2009: Advances in Artificial Intelligence, 32nd Annual German Conference on AI, Paderborn, Germany, September 15-18, 2009. Proceedings, volume 5803 of Lecture Notes in Computer Science, pages 435-443. Springer, 2009. Google Scholar
  10. Gérard P. Huet. A unification algorithm for typed lambda-calculus. Theor. Comput. Sci., 1(1):27-57, 1975. Google Scholar
  11. Don C. Jensen and Tomasz Pietrzykowski. Mechanizing omega-order type theory through unification. Theor. Comput. Sci., 3(2):123-171, 1976. Google Scholar
  12. Tomer Libal. Regular patterns in second-order unification. In Amy P. Felty and Aart Middeldorp, editors, CADE-25, volume 9195 of LNCS, pages 557-571. Springer, 2015. Google Scholar
  13. Tomer Libal and Dale Miller. Functions-as-constructors higher-order unification. In Delia Kesner and Brigitte Pientka, editors, FSCD 2016, volume 52 of LIPIcs, pages 26:1-26:17. Schloss Dagstuhl, 2016. Google Scholar
  14. Tomer Libal and Alexander Steen. Towards a substitution tree based index for higher-order resolution theorem provers. In Pascal Fontaine, Stephan Schulz, and Josef Urban, editors, IJCAR 2016, volume 1635 of CEUR-WS, pages 82-94. CEUR-WS, 2016. Google Scholar
  15. Dale Miller and Gopalan Nadathur. Programming with Higher-Order Logic. Cambridge University Press, 2012. Google Scholar
  16. Tobias Nipkow. Functional unification of higher-order patterns. In E. Best, editor, LICS '93, pages 64-74. IEEE Computer Society, 1993. Google Scholar
  17. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google Scholar
  18. Christian Prehofer. Solving higher order equations: from logic to programming. PhD thesis, Technical University Munich, Germany, 1995. Google Scholar
  19. John Alan Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1):23-41, 1965. Google Scholar
  20. Stephan Schulz. Fingerprint indexing for paramodulation and rewriting. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, IJCAR 2012, volume 7364 of LNCS, pages 477-483. Springer, 2012. Google Scholar
  21. Wayne Snyder and Jean H. Gallier. Higher-order unification revisited: Complete sets of transformations. J. Symb. Comput., 8(1/2):101-140, 1989. Google Scholar
  22. Alexander Steen and Christoph Benzmüller. The higher-order prover Leo-III. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, IJCAR 2018, volume 10900 of LNCS, pages 108-116. Springer, 2018. Google Scholar
  23. Aaron Stump, Geoff Sutcliffe, and Cesare Tinelli. Starexec: A cross-community infrastructure for logic solving. In Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, editors, IJCAR 2014, volume 8562 of LNCS, pages 367-373. Springer, 2014. Google Scholar
  24. Nik Sultana, Jasmin Christian Blanchette, and Lawrence C. Paulson. LEO-II and Satallax on the Sledgehammer test bench. J. Applied Logic, 11(1):91-102, 2013. Google Scholar
  25. Geoff Sutcliffe. The TPTP problem library and associated infrastructure - from CNF to TH0, TPTP v6.4.0. J. Autom. Reasoning, 59(4):483-502, 2017. Google Scholar
  26. Geoff Sutcliffe. The CADE-27 automated theorem proving system competition - CASC-27. AI Commun., 32(5-6):373-389, 2019. Google Scholar
  27. Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin. Efficient full higher-order unification (technical report), 2020. URL: http://matryoshka.gforge.inria.fr/pubs/hounif_report.pdf.
  28. Petar Vukmirović, Jasmin Christian Blanchette, Simon Cruanes, and Stephan Schulz. Extending a brainiac prover to lambda-free higher-order logic. In Tomás Vojnar and Lijun Zhang, editors, TACAS 2019, volume 11427 of LNCS, pages 192-210. Springer, 2019. Google Scholar
  29. Marek Zaionc. The set of unifiers in typed lambda-calculus as regular expression. In Jean-Pierre Jouannaud, editor, RTA-85, volume 202 of LNCS, pages 430-440. Springer, 1985. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact