A weakly monotonic, logically constrained, HORPO-variant

TL;DR

This paper introduces a simple, logically constrained variant of the recursive path ordering tailored for Logically Constrained Simply Typed Rewriting Systems, enhancing termination analysis in dependency pair frameworks.

Contribution

It presents a new weakly monotonic, logically constrained HORPO variant specifically designed for LCSTRSs and curried systems with logical constraints.

Findings

Handles logical constraints in rewriting systems

Supports weak monotonicity in reduction pairs

Applicable to dependency pair termination proofs

Abstract

In this short paper, we present a simple variant of the recursive path ordering, specified for Logically Constrained Simply Typed Rewriting Systems (LCSTRSs). This is a method for curried systems, without lambda but with partially applied function symbols, which can deal with logical constraints. As it is designed for use in the dependency pair framework, it is defined as reduction pair, allowing weak monotonicity.