Normal forms and normal theories in conditional rewriting

DOI10.1016/J.JLAMP.2015.06.001zbMath1356.68124OpenAlexW1140833825MaRDI QIDQ730473

Salvador Lucas, José Meseguer

Publication date: 28 December 2016

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2015.06.001

zbMATH Keywords

normal formsconditional term rewritingoperational terminationrewriting logicMaudenormal theory

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (15)

The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors ⋮ Dependency pairs for proving termination properties of conditional term rewriting systems ⋮ Symbolic Specialization of Rewriting Logic Theories with Presto ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques ⋮ Strict coherence of conditional rewriting modulo axioms ⋮ Use of logical models for proving infeasibility in term rewriting ⋮ Checking Sufficient Completeness by Inductive Theorem Proving ⋮ On Ground Convergence and Completeness of Conditional Equational Program Hierarchies ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Programming and symbolic computation in Maude ⋮ Ground confluence of order-sorted conditional specifications modulo axioms ⋮ Applications and extensions of context-sensitive rewriting ⋮ Symbolic computation in Maude: some tapas

Uses Software

• OBJ3
• CafeOBJ
• Maude

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Operational termination of conditional term rewriting systems
• Conditional rewrite rules
• Conditional rewrite rules: Confluence and termination
• Conditional rewriting logic as a unified model of concurrency
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Termination of term rewriting using dependency pairs
• Logicality of conditional rewrite systems
• Proving operational termination of membership equational programs
• Language Prototyping: An Algebraic Specification Approach
• Order-Sorted Rewriting and Congruence Closure
• Strong and Weak Operational Termination of Order-Sorted Rewrite Theories
• Rewriting Modulo SMT and Open System Analysis
• Termination Modulo Combinations of Equational Theories
• Completion of a Set of Rules Modulo a Set of Equations
• Localized Operational Termination in General Logics
• On the Completeness of Context-Sensitive Order-Sorted Specifications

This page was built for publication: Normal forms and normal theories in conditional rewriting