Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols

DOI10.1007/S10817-022-09624-4MaRDI QIDQ2090128zbMATH OpenOpenAlexFDO

Authors Franz Baader, Deepak Kapur

Publication date 24 October 2022

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s10817-022-09624-4

zbMATH Keywords

description logicsextensionalityinterpreted function symbolsordered rewritingsemantic congruence closureshallow identitiesword problem for ground identities

Mathematics Subject Classification ID

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

Recommendations

• Deciding the word problem for ground identities with commutative and extensional symbols
• On ground word problem of term equation systems
• THE WORD PROBLEM OF ACD-GROUND THEORIES IS UNDECIDABLE
• scientific article; zbMATH DE number 58292
• Decidability and complexity analysis by basic paramodulation

Cites work

• A fast algorithm for generating reduced ground rewriting systems from a set of ground equations
• A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
• An algorithm for finding canonical sets of ground rewrite rules in polynomial time
• An algorithm for reasoning about equality
• An introduction to description logic
• Any ground associative-commutative theory has a finite canonical system
• Automatic decidability and combinability
• Conditional congruence closure over uninterpreted and interpreted symbols
• Deciding the word problem for ground identities with commutative and extensional symbols
• Fast congruence closure and extensions
• Fast Decision Procedures Based on Congruence Closure
• scientific article; zbMATH DE number 3930347 (Why is no real title available?)
• scientific article; zbMATH DE number 3688778 (Why is no real title available?)
• scientific article; zbMATH DE number 50648 (Why is no real title available?)
• scientific article; zbMATH DE number 51770 (Why is no real title available?)
• scientific article; zbMATH DE number 1538018 (Why is no real title available?)
• scientific article; zbMATH DE number 3301426 (Why is no real title available?)
• scientific article; zbMATH DE number 7700620 (Why is no real title available?)
• Modal tableau systems with blocking and congruence closure
• Ordered rewriting and confluence
• Shostak's congruence closure as completion
• Syntacticness, cycle-syntacticness and shallow theories
• Term Rewriting and All That
• The complexity of the word problems for commutative semigroups and polynomial ideals
• The theorem prover of the program verifier Tatzelwurm
• Variations on the Common Subexpression Problem

Cited in

(3)

• Deciding the word problem for ground identities with commutative and extensional symbols
• Tail reduction free term rewriting systems revisited
• Congruence closure modulo groups

This page was built for publication: Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols

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