Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols
From MaRDI portal
Publication:2090128
DOI10.1007/s10817-022-09624-4OpenAlexW4229336319MaRDI QIDQ2090128
Publication date: 24 October 2022
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-022-09624-4
extensionalitydescription logicsordered rewritinginterpreted function symbolssemantic congruence closureshallow identitiesword problem for ground identities
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Automatic decidability and combinability
- A fast algorithm for generating reduced ground rewriting systems from a set of ground equations
- Fast congruence closure and extensions
- Syntacticness, cycle-syntacticness and shallow theories
- Any ground associative-commutative theory has a finite canonical system
- Conditional congruence closure over uninterpreted and interpreted symbols
- The complexity of the word problems for commutative semigroups and polynomial ideals
- Deciding the word problem for ground identities with commutative and extensional symbols
- An Introduction to Description Logic
- Modal Tableau Systems with Blocking and Congruence Closure
- Fast Decision Procedures Based on Congruence Closure
- 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
- Term Rewriting and All That
- A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
This page was built for publication: Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols
