ELAN from a rewriting logic point of view
type: Item
instance of: scholarly article
title: ELAN from a rewriting logic point of view
zbMATH Open document ID: 1001.68057
DOI: 10.1016/S0304-3975(01)00358-9
author: Peter Borovanský
author: Claude Kirchner
author: Hélène Kirchner
author: Pierre-Etienne Moreau
published in: Theoretical Computer Science
publication date: 2002-08-13T00:00:00Z
Mathematics Subject Classification ID: 68Q42
Mathematics Subject Classification ID: 68T27
zbMATH DE Number: 1780619
zbMATH Keywords: computational system
zbMATH Keywords: conditional rewriting logic
zbMATH Keywords: strategy theory
zbMATH Keywords: rule-based programming
zbMATH Keywords: rewriting calculus
describes a project that uses: ELAN
describes a project that uses: Maude
describes a project that uses: LCF
MaRDI profile type: Publication
cites work: The B-Book
cites work: Proving innermost normalisation automatically
cites work: Associative-commutative discrimination nets
cites work: Basic paramodulation
cites work: Autarkic computations in formal proofs
cites work: Complexity of matching problems
cites work: Q4222858
cites work: REWRITING WITH STRATEGIES IN $\mathsf{ELAN}$: A FUNCTIONAL SEMANTICS
cites work: Q4222861
cites work: Q4264200
cites work: Combining higher-order and first-order computation using \(\rho\)-calculus: Towards a semantics of ELAN
cites work: The simply typed rewriting calculus
cites work: Q2778872
cites work: Q2769430
cites work: Q4222979
cites work: Q4385532
cites work: 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\)
cites work: Theorem proving modulo
cites work: Induction for termination with local strategies
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: On proving termination by innermost termination
cites work: Completion of a Set of Rules Modulo a Set of Equations
cites work: Promoting rewriting to a programming language: A compiler for non-deterministic rewrite programs in associative-commutative theories
cites work: Q4264199
cites work: Q2736358
cites work: Tree automata help one to solve equational formulae in AC-theories
cites work: Q3032225
cites work: Conditional rewriting logic as a unified model of concurrency
cites work: Complete Sets of Reductions for Some Equational Theories
cites work: Prototyping combination of unification algorithms with the ELAN rule-based programming language
cites work: Automated deduction with associative-commutative operators
full work available at URL: s0304-3975(01)00358-9
OpenAlex ID: W2147892488
description: scientific article; zbMATH DE number 1780619