2024/06/27 by Liye Guo, Guo, Liye, Kasper Hagens +5
Computer Science · #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · pdf · doi:10.48550/arxiv.2406.19379
openalex publication_date 2024/06/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Dependency pairs constitute a series of very effective techniques for the termination analysis of term rewriting systems. In this paper, we adapt the static dependency pair framework to logically constrained simply-typed term rewriting systems (LCSTRSs), a higher-order formalism with logical constraints built in. We also propose the concept of universal computability, which enables a form of open-world termination analysis through the use of static dependency pairs.