Conditional rewrite rules: Confluence and termination

DOI10.1016/0022-0000(86)90033-4zbMath0658.68031MaRDI 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

zbMATH Keywords

algebraic specifications; confluence; termination; term rewriting systems; reduction techniques; conditional rewrite rules

Mathematics Subject Classification ID

68Q65: Abstract data types; algebraic specification

68T99: Artificial intelligence

Related Items

Unique normal form property of compatible term rewriting systems: A new proof of Chew's theorem, Implementing conditional term rewriting by graph rewriting, 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, Conditional linearization, Equational type logic, A completion procedure for conditional equations, Implementing term rewrite languages in DACTL, A rationale for conditional equational programming, Conditional equational theories and complete sets of transformations, Conditional rewrite rules, Rewrite method for theorem proving in first order theory with equality, Simplifying conditional term rewriting systems: Unification, termination and confluence, Sequentiality in orthogonal term rewriting systems, Term-rewriting systems with rule priorities, 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, Completeness results for basic narrowing, Incremental constraint satisfaction for equational logic programming, Equational rules for rewriting logic, Perpetuality and uniform normalization in orthogonal rewrite systems, Elimination of conditions, Logicality of conditional rewrite systems, Nominal rewriting, Evaluation strategies for functional logic programming, Shallow confluence of conditional term rewriting systems, Kernel-LEAF: A logic plus functional language

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• Conditional rewrite rules
• Computing in systems described by equations
• Initial Algebra Semantics and Continuous Algebras
• Minimal and Optimal Computations of Recursive Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item