Order-Sorted Rewriting and Congruence Closure

Cites Work

All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
A mechanical solution of Schubert's steamroller by many-sorted resolution
Complexity, convexity and combinations of theories
Simplification by Cooperating Decision Procedures
Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
Variations on the Common Subexpression Problem
An algorithm for finding canonical sets of ground rewrite rules in polynomial time
Title not available (Why is that?)
Fast Decision Procedures Based on Congruence Closure
Title not available (Why is that?)
CafeOBJ Report. The language, proof techniques, and methodologies for object-oriented algebraicspecification
Title not available (Why is that?)
Specification and proof in membership equational logic
Shostak's congruence closure as completion
Deciding Combinations of Theories
Logics in Artificial Intelligence
Solvable cases of the decision problem
Inheritance hierarchies: Semantics and unifications
Computational aspects of an order-sorted logic with term declarations
Title not available (Why is that?)
Title not available (Why is that?)
The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning
Order-Sorted Rewriting and Congruence Closure
An algorithm for reasoning about equality
Equational completion in order-sorted algebras
Abstract congruence closure
Any ground associative-commutative theory has a finite canonical system
Combining Equational Reasoning
Canonized rewriting and ground AC completion modulo Shostak theories: design and implementation

Cited In (12)

Abstract domains for reordering CLP(RLin) programs
A semantic approach to order-sorted rewriting
A partial evaluation framework for order-sorted equational programs modulo axioms
Currying of order-sorted term rewriting systems
Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems
Title not available (Why is that?)
On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms*
Order-Sorted Parameterization and Induction
Normal forms and normal theories in conditional rewriting
Order-Sorted Rewriting and Congruence Closure
Bi-rewriting, a term rewriting technique for monotonic order relations

Uses Software

CafeOBJ
Maude

   Recommendations

This page was built for publication: Order-Sorted Rewriting and Congruence Closure

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2811360)