Deciding the word problem for ground identities with commutative and extensional symbols

DOI10.1007/978-3-030-51074-9_10OpenAlexW3039259551MaRDI QIDQ2096444

Franz Baader, Deepak Kapur

Publication date: 9 November 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-51074-9_10

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties ⋮ Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols

Cites Work

• A fast algorithm for generating reduced ground rewriting systems from a set of ground equations
• Fast congruence closure and extensions
• Conditional congruence closure over uninterpreted and interpreted 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
• Any ground associative-commutative theory has a finite canonical system
• Unnamed Item
• Unnamed Item