vix.ing · top · new · best · stats · spec

A weakly monotonic, logically constrained, HORPO-variant

2024/06/26 by Cynthia Kop, Kop, Cynthia
Computer Science · #Distributed and Parallel Computing Systems #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Real-Time Systems Scheduling

paper · pdf · doi:10.48550/arxiv.2406.18493

openalex publication_date 2024/06/26 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Related