Abstract
© P. Vukmirović, A. Bentkamp, and V. Nummelin.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, together with new higher-order term indexing data structures, is implemented in the Zipperposi-tion theorem prover. Experimental evaluation shows a clear advantage over Jensen and Pietrzykowski’s procedure.
| Original language | English |
|---|---|
| Article number | 18 |
| Journal | Logical Methods in Computer Science |
| Volume | 17 |
| Issue number | 4 |
| DOIs | |
| Publication status | Published - 2021 |
Funding
Acknowledgement. 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ˇcić, Robert Lewis, Femke van Raamsdonk, Hans-Jörg Schurr, Sophie Tourret, Dmitriy Traytel, and the anonymous reviewers for suggesting many improvements to this text. 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).
| Funders | Funder number |
|---|---|
| Horizon 2020 Framework Programme | 713999 |
| European Research Council | |
| Nederlandse Organisatie voor Wetenschappelijk Onderzoek | 016 |