Derivational complexity and context-sensitive Rewriting
type: Item
instance of: scholarly article
title: Derivational complexity and context-sensitive Rewriting
author: Salvador Lucas
published in: Journal of Automated Reasoning
publication date: 2022-01-21T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7461269
zbMATH Keywords: derivational complexity
zbMATH Keywords: term rewriting
zbMATH Keywords: termination
describes a project that uses: Haskell
describes a project that uses: OBJ3
describes a project that uses: CoCoWeb
describes a project that uses: Cops
describes a project that uses: FORT
describes a project that uses: Maude
describes a project that uses: AProVE
MaRDI profile type: Publication
full work available at URL: s10817-021-09603-1
OpenAlex ID: W3193667803
cites work: Termination of term rewriting using dependency pairs
cites work: Term Rewriting and All That
cites work: Q4263809
cites work: Algorithms with polynomial interpretation termination proof
cites work: Q4264735
cites work: All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
cites work: Mechanically proving termination using polynomial interpretations
cites work: Q4385535
cites work: A note on simplification orderings
cites work: Programming and symbolic computation in Maude
cites work: Matrix interpretations for proving termination of term rewriting
cites work: Mechanizing and improving dependency pairs
cites work: Analyzing program termination and complexity automatically with \textsf{AProVE}
cites work: mu-term: Verify Termination Properties Automatically (System Description)
cites work: Automated Complexity Analysis Based on the Dependency Pair Method
cites work: Automated Complexity Analysis Based on Context-Sensitive Rewriting
cites work: Automated reasoning. 9th international joint conference, IJCAR 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14--17, 2018. Proceedings
cites work: Termination proofs by multiset path orderings imply primitive recursive derivation lengths
cites work: Termination proofs and the length of derivations
cites work: Q5581665
cites work: Context-sensitive rewriting strategies
cites work: Q4808754
cites work: Polynomials over the reals in proofs of termination : from theory to practice
cites work: Applications and extensions of context-sensitive rewriting
cites work: The Derivational Complexity Induced by the Dependency Pair Method
cites work: Complexity Analysis of Term Rewriting Based on Matrix and Context Dependent Interpretations
cites work: Revisiting Matrix Interpretations for Proving Termination of Term Rewriting
cites work: Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting
cites work: Analyzing innermost runtime complexity of term rewriting by dependency pairs
cites work: Q2783416
cites work: Synthesis of sup-interpretations: a survey
cites work: Classes of Predictably Computable Functions
cites work: Parameterized strategies specification in Maude
cites work: Q4256647
cites work: Signature Extensions Preserve Termination
cites work: Q4799892
cites work: POLYNOMIALLY BOUNDED MATRIX INTERPRETATIONS
cites work: Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths
cites work: Termination of term rewriting: Interpretation and type elimination
cites work: Termination of context-sensitive rewriting
DOI: 10.1007/S10817-021-09603-1
description: scientific article; zbMATH DE number 7461269