Order-Sorted Rewriting and Congruence Closure
From MaRDI portal
Publication:2811360
DOI10.1007/978-3-662-49630-5_29zbMath1475.68142OpenAlexW2467885142MaRDI QIDQ2811360
Publication date: 10 June 2016
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-662-49630-5_29
Related Items (4)
Normal forms and normal theories in conditional rewriting ⋮ A partial evaluation framework for order-sorted equational programs modulo axioms ⋮ Order-Sorted Rewriting and Congruence Closure ⋮ Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms*
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Equational completion in order-sorted algebras
- 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
- Inheritance hierarchies: Semantics and unifications
- Complexity, convexity and combinations of theories
- The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Any ground associative-commutative theory has a finite canonical system
- Abstract congruence closure
- Computational aspects of an order-sorted logic with term declarations
- Specification and proof in membership equational logic
- Solvable cases of the decision problem
- Order-Sorted Rewriting and Congruence Closure
- Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation
- Combining Equational Reasoning
- Deciding Combinations of Theories
- Fast Decision Procedures Based on Congruence Closure
- Simplification by Cooperating Decision Procedures
- Variations on the Common Subexpression Problem
- An algorithm for finding canonical sets of ground rewrite rules in polynomial time
- An algorithm for reasoning about equality
- Shostak's congruence closure as completion
- Logics in Artificial Intelligence
This page was built for publication: Order-Sorted Rewriting and Congruence Closure