6 papers
Unification of Deterministic Higher-Order Patterns (Full Version)
Johannes Niederhauser, Aart Middeldorp
We present a sound and complete unification procedure for deterministic higher-order patterns, a class of simply-typed lambda terms introduced by Yokoyama et al. which comes with a…
Towards an HRS Category in TermCOMP
Johannes Niederhauser, Aart Middeldorp
We show that there is a simple syntactically-defined subclass of higher-order benchmarks in the termination problem database for which rewriting according to Nipkow's higher-order…
Hydra Battles and AC Termination
Nao Hirokawa, Aart Middeldorp
We present a new encoding of the Battle of Hercules and Hydra as a rewrite system with AC symbols. Unlike earlier term rewriting encodings, it faithfully models any strategy of Her…
The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting (Full Version)
Johannes Niederhauser, Aart Middeldorp
We lift the computability path order and its extensions from plain higher-order rewriting to higher-order rewriting on beta-eta-normal forms where matching modulo beta-eta is emplo…
Automated Analysis of Logically Constrained Rewrite Systems using crest
Jonas Schöpf, Aart Middeldorp
We present crest, a tool for automatically proving (non-)confluence and termination of logically constrained rewrite systems. We compare crest to other tools for logically constrai…
Left-Linear Completion with AC Axioms
Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp
We revisit completion modulo equational theories for left-linear term rewrite systems where unification modulo the theory is avoided and the normal rewrite relation can be used in…