Equational completion in order-sorted algebras

DOI10.1016/0304-3975(90)90034-FzbMath0698.68028MaRDI QIDQ912606

Claude Kirchner, Hélène Kirchner, Isabelle Gnaedig

Publication date: 1990

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

zbMATH Keywords

completion proceduresequational term rewriting systemsorder-sorted algebrasorder-sorted equational logic

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Abstract data types; algebraic specification (68Q65) Equational logic, Mal'tsev conditions (08B05) Thue and Post systems, etc. (03D03)

Related Items (8)

Confluence of terminating membership conditional TRS ⋮ Meta-rule synthesis from crossed rewrite systems ⋮ On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories ⋮ Dynamically-typed computations for order-sorted equational presentations ⋮ Specification and proof in membership equational logic ⋮ Semantics of order-sorted specifications ⋮ From Search to Computation: Redundancy Criteria and Simplification at Work ⋮ Order-Sorted Rewriting and Congruence Closure

Uses Software

• Miranda
• REVE

Cites Work

• Orderings for term-rewriting systems
• Investigations in many-sorted quantor logic
• Proofs by induction in equational theories with constructors
• Rewrite systems on a lattice of types
• REVEUR-3: The implementation of a general completion procedure parameterized by built-in theories and strategies
• Termination of rewriting
• New decision algorithms for finitely presented commutative semigroups
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• On multiset orderings
• Order-sorted completion: The many-sorted way
• Semantics of order-sorted specifications
• On theories with a combinatorial definition of 'equivalence'
• Completion of a Set of Rules Modulo a Set of Equations
• Proving termination with multiset orderings
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Complete Sets of Reductions for Some Equational Theories
• Programming with Equations
• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Equational completion in order-sorted algebras