Counterexamples to termination for the direct sum of term rewriting systems

From MaRDI portal
Publication:1107975

DOI10.1016/0020-0190(87)90122-0zbMath0653.68010OpenAlexW2080725351WikidataQ56019617 ScholiaQ56019617MaRDI QIDQ1107975

Yoshihito Toyama

Publication date: 1987

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2433/99946



Related Items

Decidability of reachability for disjoint union of term rewriting systems, Collapsed tree rewriting: Completeness, confluence, and modularity, Combinations of simplifying conditional term rewriting systems, Type removal in term rewriting, Termination of term rewriting by interpretation, Confluence of the disjoint union of conditional term rewriting systems, Implementing term rewriting by graph reduction: Termination of combined systems, Generalized sufficient conditions for modular termination of rewriting, Modular aspects of properties of term rewriting systems related to normal forms, Termination for the direct sum of left-linear term rewriting systems, Modularity of termination in term graph rewriting, On the modularity of termination of term rewriting systems, Modular proofs for completeness of hierarchical term rewriting systems, Modular and incremental proofs of AC-termination, On termination of the direct sum of term-rewriting systems, Automatic synthesis of logical models for order-sorted first-order theories, Tyrolean termination tool: techniques and features, Mechanizing and improving dependency pairs, Bubbles in modularity, An improved general path order, Modularity in term rewriting revisited, Jumping and escaping: modular termination and the abstract path ordering, Interaction nets and term-rewriting systems, Semi-completeness of hierarchical and super-hierarchical combinations of term rewriting systems, Simple termination of rewrite systems, Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility, Analyzing Innermost Runtime Complexity Through Tuple Interpretations, Deciding the word problem in the union of equational theories., Modular term rewriting systems and the termination, Proving termination by dependency pairs and inductive theorem proving, Modular Termination of Basic Narrowing, Maximal Termination, Root-Labeling, Overlap closures do not suffice for termination of general term rewriting systems, Some classes of term rewriting systems inferable from positive data, Modularity of termination and confluence in combinations of rewrite systems with λω, Termination of term rewriting using dependency pairs, On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems, Intersection type assignment systems with higher-order algebraic rewriting, Modular termination of \(r\)-consistent and left-linear term rewriting systems, Completeness of combinations of conditional constructor systems, Modularity in noncopying term rewriting, Loop detection in term rewriting using the eliminating unfoldings, Termination is not modular for confluent variable-preserving term rewriting systems, Proof certificates for equality reasoning, Extension orderings, Transforming termination by self-labelling, Modularity of simple termination of term rewriting systems with shared constructors, A domain model characterising strong normalisation, Essentials of Term Graph Rewriting, Automating the dependency pair method, On modularity in infinitary term rewriting, Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness, Unnamed Item, Variant-Based Satisfiability in Initial Algebras, Completeness of combinations of constructor systems, Modular termination of prefix-constrained term rewrite systems, Modular aspects of term graph rewriting, A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method, Termination of narrowing revisited, Some characteristics of strong innermost normalization, A uniform framework for term and graph rewriting applied to combined systems, The size-change principle and dependency pairs for termination of term rewriting, Modular and incremental automated termination proofs, Modular termination proofs for rewriting using dependency pairs



Cites Work