Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs
Explore this paper's citation graph
Summary
This work gives the first mechanized proof of the fact that for showing termination of a term rewrite system, it may restrict to well-formed terms using just the function symbols actually occurring in the rules of the system.
- Type
- article
- Published
- 2010-08-23
- Cited by
- 16
- References
- 12
- OpenAlex
- https://openalex.org/W1554961415
- Semantic Scholar
- https://api.semanticscholar.org/CorpusID:14277255
Keywords
Mathematical proof, Signature (topology), Dependency (UML), Computer science, Counterexample
References
- A simple proof of sufficient conditions for the termination of the disjoint union of term rewriting systems
- Term rewriting and all that
- Mechanizing and Improving Dependency Pairs
- Termination of term rewriting using dependency pairs
- Isabelle/HOL
- TERMINATION OF TERM REWRITING BY SEMANTIC LABELLING
- The DP framework for proving termination of term rewriting
- Root-Labeling
- Certification of Termination Proofs Using CeTA
Cited by
- Modularity in term rewriting revisited
- Uncurrying for Termination and Complexity
- Automated verification of termination certificates. (Vérification automatique de certificats de terminaison)
- Modular and Certified Semantic Labeling and Unlabeling
- Dependency pairs for proving termination properties of conditional term rewriting systems
- Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion
- Size-based termination of higher-order rewriting
- Formalizing the Dependency Pair Criterion for Innermost Termination
- Derivational Complexity and Context-Sensitive Rewriting
- Simulating Dependency Pairs by Semantic Labeling
- Team FORMES FOrmal Methods for Embedded Systems
- Generalized and Formalized Uncurrying
- On Modularity of Termination Properties of Rewriting under Strategies
- Formalizing Bounded Increase
- Certification of Nontermination Proofs
- Certified Equational Reasoning via Ordered Completion