3 papers
cs.LO2026
Beyond Absolute Positiveness for Universally Quantified Non-Linear Polynomial Constraints
Carsten Fuhs
Polynomial interpretations from function symbols to natural numbers induce a prominent class of monotone algebras and corresponding well-founded orders on terms, used, e.g., for te…
cs.LO2025
Verifying Procedural Programs via Constrained Rewriting Induction
Carsten Fuhs, Cynthia Kop, Naoki Nishida
This paper aims to develop a verification method for procedural programs via a transformation into Logically Constrained Term Rewriting Systems (LCTRSs). To this end, we extend tra…
cs.LO2024
On Complexity Bounds and Confluence of Parallel Term Rewriting
Thaïs Baudon, Carsten Fuhs, Laure Gonnord
We revisit parallel-innermost term rewriting as a model of parallel computation on inductive data structures and provide a corresponding notion of runtime complexity parametric in…