Termination of LCTRSs

2016/01/13 by Cynthia Kop, Kop, Cynthia · 1 citation
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Natural Language Processing Techniques #Semantic Web and Ontologies

paper · pdf · doi:10.48550/arxiv.1601.03206

openalex publication_date 2016/01/13 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

Logically Constrained Term Rewriting Systems (LCTRSs) provide a general framework for term rewriting with constraints. We discuss a simple dependency pair approach to prove termination of LCTRSs. We see that existing techniques transfer to the constrained setting in a natural way.

Cited by

• Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations (Full Version)

Related

• Higher-Order Constrained Dependency Pairs for (Universal) Computability
• Higher-Order LCTRSs and Their Termination
• A Dependency Pair Framework for Relative Termination of Term Rewriting
• Inductive Theorem Proving meets Dependency Pairs
• Proving and Disproving Termination in the Dependency Pair Framework