Decreasing diagrams and relative termination
type: Item
instance of: scholarly article
title: Decreasing diagrams and relative termination
zbMATH Open document ID: 1243.68199
author: Nao Hirokawa
author: Aart Middeldorp
published in: Journal of Automated Reasoning
publication date: 2012-07-31T00:00:00Z
Mathematics Subject Classification ID: 68Q42
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 6062058
zbMATH Keywords: confluence
zbMATH Keywords: decreasing diagrams
zbMATH Keywords: relative termination
zbMATH Keywords: term rewriting
describes a project that uses: Isabelle/HOL
describes a project that uses: Tyrolean
MaRDI profile type: Publication
full work available at URL: s10817-011-9238-x
OpenAlex ID: W1997678912
cites work: Automated Confluence Proof by Decreasing Diagrams based on Rule-Labelling.
cites work: Q4520528
cites work: A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems
cites work: Proving Confluence of Term Rewriting Systems Automatically
cites work: Solving Partial Order Constraints for LPO Termination
cites work: Combinatory logic. Vol. II
cites work: Matrix interpretations for proving termination of term rewriting
cites work: Q4253320
cites work: On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems
cites work: Generalizing Newman’s Lemma for Left-Linear Rewrite Systems
cites work: Decreasing Diagrams and Relative Termination
cites work: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
cites work: Q5581665
cites work: Higher-order rewrite systems and their confluence
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Modular properties of composable term rewriting systems
cites work: Q2783416
cites work: Confluence by decreasing diagrams
cites work: Developing developments
cites work: Confluence by Decreasing Diagrams
cites work: Tree-Manipulating Systems and Church-Rosser Theorems
cites work: Labelings for Decreasing Diagrams.
cites work: KBO orientability
cites work: Modular Complexity Analysis via Relative Complexity
cites work: Satisfiability of Non-linear (Ir)rational Arithmetic
DOI: 10.1007/S10817-011-9238-X
description: scientific article; zbMATH DE number 6062058