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

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

Authors: 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

Recommendations

• Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols
• THE WORD PROBLEM OF ACD-GROUND THEORIES IS UNDECIDABLE
• A decision problem for varieties of commutative semigroups
• On ground AC-completion
• scientific article; zbMATH DE number 3930347

Mathematics Subject Classification ID

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

Cites Work

• Variations on the Common Subexpression Problem
• An algorithm for finding canonical sets of ground rewrite rules in polynomial time
• Term Rewriting and All That
• Fast Decision Procedures Based on Congruence Closure
• Shostak's congruence closure as completion
• A fast algorithm for generating reduced ground rewriting systems from a set of ground equations
• Title not available (Why is that?)
• Any ground associative-commutative theory has a finite canonical system
• An introduction to description logic
• Fast congruence closure and extensions
• An algorithm for reasoning about equality
• Title not available (Why is that?)
• Conditional congruence closure over uninterpreted and interpreted symbols
• Modal tableau systems with blocking and congruence closure
• The theorem prover of the program verifier Tatzelwurm

Cited In (2)

• 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

This page was built for publication: Deciding the word problem for ground identities with commutative and extensional symbols

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