Abstract
The embedding path order, introduced in this article, is a variant of the recursive path order (RPO) for untyped λ-free higher-order terms (also called applicative first-order terms). Unlike other higher-order variants of RPO, it is a ground-total and well-founded simplification order, making it more suitable for the superposition calculus. I formally proved the order’s theoretical properties in Isabelle/HOL and evaluated the order in a prototype based on the superposition prover Zipperposition.
| Original language | English |
|---|---|
| Pages (from-to) | 2447-2470 |
| Number of pages | 24 |
| Journal | Journal of applied logistics |
| Volume | 8 |
| Issue number | 10 |
| Early online date | 1 Dec 2021 |
| DOIs | |
| Publication status | Published - Dec 2021 |
Bibliographical note
ISBN: 978-1-84890-381-4.Funding Information:
I am grateful to the maintainers of StarExec Iowa for letting me use their service; to Jasmin Blanchette for his excellent supervision and for providing benchmarks; to Ahmed Bhayat, Simon Cruanes, Wan Fokkink, Carsten Fuhs, andPetar Vukmirović for the stimulating discussions and the constructive feedback; to Jürgen Giesl and Femke van Raamsdonk for pointers to the literature; and to the anonymous reviewers for suggesting many improvements to this text. My 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). It has also been funded by a Chinese Academy of Sciences President’s International Fellowship for Postdoctoral Researchers (grant No. 2021PT0015).
Publisher Copyright:
© 2021, College Publications. All rights reserved.
Funding
I am grateful to the maintainers of StarExec Iowa for letting me use their service; to Jasmin Blanchette for his excellent supervision and for providing benchmarks; to Ahmed Bhayat, Simon Cruanes, Wan Fokkink, Carsten Fuhs, andPetar Vukmirović for the stimulating discussions and the constructive feedback; to Jürgen Giesl and Femke van Raamsdonk for pointers to the literature; and to the anonymous reviewers for suggesting many improvements to this text. My 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). It has also been funded by a Chinese Academy of Sciences President’s International Fellowship for Postdoctoral Researchers (grant No. 2021PT0015).