Conditional rewrite rules: Confluence and termination
From MaRDI portal
Publication:1111368
DOI10.1016/0022-0000(86)90033-4zbMath0658.68031OpenAlexW2167316540MaRDI QIDQ1111368
Jan A. Bergstra, Jan Willem Klop
Publication date: 1986
Published in: Journal of Computer and System Sciences (Search for Journal in Brave)
Full work available at URL: https://dspace.library.uu.nl/handle/1874/12720
algebraic specificationsconfluenceterminationterm rewriting systemsreduction techniquesconditional rewrite rules
Related Items (57)
Confluence of terminating membership conditional TRS ⋮ Extended term rewriting systems ⋮ Confluence of the disjoint union of conditional term rewriting systems ⋮ Completeness results for basic narrowing ⋮ Nominal rewriting ⋮ The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors ⋮ Completion-time optimization of rewrite-time goal solving ⋮ Priority rewriting: Semantics, confluence, and conditionals ⋮ Negation with logical variables in conditional rewriting ⋮ Open problems in rewriting ⋮ Level-confluence of conditional rewrite systems with extra variables in right-hand sides ⋮ Confluence of terminating conditional rewrite systems revisited ⋮ Rewrite method for theorem proving in first order theory with equality ⋮ Simplifying conditional term rewriting systems: Unification, termination and confluence ⋮ Kernel-LEAF: A logic plus functional language ⋮ Transformations of Conditional Rewrite Systems Revisited ⋮ Dependency pairs for proving termination properties of conditional term rewriting systems ⋮ Incremental constraint satisfaction for equational logic programming ⋮ Rewriting systems over similarity and generalized pseudometric spaces and their properties ⋮ Determinization of conditional term rewriting systems ⋮ Reversible computation in term rewriting ⋮ Levels of undecidability in rewriting ⋮ Implementing term rewrite languages in DACTL ⋮ A rationale for conditional equational programming ⋮ Conditional equational theories and complete sets of transformations ⋮ Inverse Unfold Problem and Its Heuristic Solving ⋮ Notes on Structure-Preserving Transformations of Conditional Term Rewrite Systems ⋮ Evaluation strategies for functional logic programming ⋮ Elimination of conditions ⋮ Logicality of conditional rewrite systems ⋮ Sequentiality in orthogonal term rewriting systems ⋮ A sequential reduction strategy ⋮ On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems ⋮ A combinatory logic approach to higher-order E-unification ⋮ Strict coherence of conditional rewriting modulo axioms ⋮ Functional Logic Programming: From Theory to Curry ⋮ Conditional linearization ⋮ Unique normal form property of compatible term rewriting systems: A new proof of Chew's theorem ⋮ On the confluence of lambda-calculus with conditional rewriting ⋮ Implementing conditional term rewriting by graph rewriting ⋮ Normal forms and normal theories in conditional rewriting ⋮ Shallow confluence of conditional term rewriting systems ⋮ Applications and extensions of context-sensitive rewriting ⋮ Term-rewriting systems with rule priorities ⋮ Equational type logic ⋮ A completion procedure for conditional equations ⋮ Characterizing Compatible View Updates in Syntactic Bidirectionalization ⋮ Evaluation Strategies for Functional Logic Programming ⋮ Operational termination of conditional term rewriting systems ⋮ Perpetuality and uniform normalization in orthogonal rewrite systems ⋮ Transformation for Refining Unraveled Conditional Term Rewriting Systems ⋮ Conditional rewrite rules ⋮ Equational rules for rewriting logic ⋮ Deductive and inductive synthesis of equational programs ⋮ Origin tracking ⋮ Contextual rewriting as a sound and complete proof method for conditional LOG-specifications ⋮ Proving termination of (conditional) rewrite systems. A semantic approach
Cites Work
This page was built for publication: Conditional rewrite rules: Confluence and termination
