ELAN from a rewriting logic point of view

DOI10.1016/S0304-3975(01)00358-9zbMath1001.68057OpenAlexW2147892488MaRDI QIDQ1608914

Pierre-Etienne Moreau, Peter Borovanský, Hélène Kirchner, Claude Kirchner

Publication date: 13 August 2002

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(01)00358-9

zbMATH Keywords

rule-based programmingcomputational systemconditional rewriting logicrewriting calculusstrategy theory

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Grammars and rewriting systems (68Q42)

Related Items

Rewriting logic: Roadmap and bibliography, Invariant-driven specifications in Maude, Algebraic simulations, Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic, A rewriting logic framework for operational semantics of membrane systems, An integrated framework for the diagnosis and correction of rule-based programs, Rewriting Strategies and Strategic Rewrite Programs, Twenty years of rewriting logic, Strategy based semantics for mobility with time and access permissions, A modular order-sorted equational generalization algorithm, MTT: The Maude Termination Tool (System Description), A survey of strategies in rule-based program transformation systems, Equational abstractions, Model Checking TLR* Guarantee Formulas on Infinite Systems, Strict coherence of conditional rewriting modulo axioms, Strategy-Based Proof Calculus for Membrane Systems, A Rewriting Semantics for Maude Strategies, Characterizing and proving operational termination of deterministic conditional term rewriting systems, Proving operational termination of membership equational programs, A Modular Equational Generalization Algorithm, Methods for Proving Termination of Rewriting-based Programming Languages by Transformation, A rewriting logic approach to operational semantics, Order-Sorted Generalization, Foundations of the rule-based system ρLog, Operational termination of conditional term rewriting systems, Distributive ρ-calculus

Uses Software

• ELAN
• Maude
• LCF

Cites Work

• Complexity of matching problems
• A technical note on AC-unification. The number of minimal unifiers of the equation \(\alpha x_ 1+ \cdots + \alpha x_ p \doteq _{AC} \beta y_ 1+ \cdots + \beta y_ q\)
• Conditional rewriting logic as a unified model of concurrency
• Automated deduction with associative-commutative operators
• Theorem proving modulo
• Autarkic computations in formal proofs
• Edinburgh LCF. A mechanized logic of computation
• Tree automata help one to solve equational formulae in AC-theories
• Basic paramodulation
• Induction for termination with local strategies
• Completion of a Set of Rules Modulo a Set of Equations
• Complete Sets of Reductions for Some Equational Theories
• The B-Book
• Proving innermost normalisation automatically
• Prototyping combination of unification algorithms with the ELAN rule-based programming language
• Associative-commutative discrimination nets
• On proving termination by innermost termination
• REWRITING WITH STRATEGIES IN $\mathsf{ELAN}$: A FUNCTIONAL SEMANTICS
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item