10 citations · 51 across the 22 of their papers we have counts for
22 papers
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…
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…
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…
Confluence of Logically Constrained Rewrite Systems Revisited
Jonas Schöpf, Fabian Mitterwallner, Aart Middeldorp
We show that (local) confluence of terminating locally constrained rewrite systems is undecidable, even when the underlying theory is decidable. Several confluence criteria for log…