Equational completion in order-sorted algebras
From MaRDI portal
Publication:912606
DOI10.1016/0304-3975(90)90034-FzbMath0698.68028MaRDI QIDQ912606
Hélène Kirchner, Isabelle Gnaedig, Claude Kirchner
Publication date: 1990
Published in: Theoretical Computer Science (Search for Journal in Brave)
completion procedures; equational term rewriting systems; order-sorted algebras; order-sorted equational logic
68W30: Symbolic computation and algebraic computation
68Q65: Abstract data types; algebraic specification
08B05: Equational logic, Mal'tsev conditions
03D03: Thue and Post systems, etc.
Related Items
Uses Software
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