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

DOI10.1007/S10817-022-09624-4OpenAlexW4229336319MaRDI QIDQ2090128FDOQ2090128

Authors: Franz Baader, Deepak Kapur 

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

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

zbMATH Keywords

description logicsextensionalityordered rewritinginterpreted function symbolssemantic congruence closureshallow identitiesword problem for ground identities

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
• Automatic decidability and combinability
• Title not available (Why is that?)
• Fast Decision Procedures Based on Congruence Closure
• The complexity of the word problems for commutative semigroups and polynomial ideals
• Title not available (Why is that?)
• 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?)
• Ordered rewriting and confluence
• Title not available (Why is that?)
• Syntacticness, cycle-syntacticness and shallow theories
• An introduction to description logic
• Fast congruence closure and extensions
• An algorithm for reasoning about equality
• Title not available (Why is that?)
• Any ground associative-commutative theory has a finite canonical system
• Conditional congruence closure over uninterpreted and interpreted symbols
• A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
• Deciding the word problem for ground identities with commutative and extensional symbols
• Modal tableau systems with blocking and congruence closure
• Title not available (Why is that?)
• Title not available (Why is that?)
• The theorem prover of the program verifier Tatzelwurm

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)