Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols
Pages 163 - 180
Abstract
The word problem for a finite set of ground identities is known to be decidable in polynomial time, and this is also the case if some of the function symbols are assumed to be commutative. We show that decidability in P is preserved if we also assume that certain function symbols f are extensional in the sense that implies . In addition, we investigate a variant of extensionality that is more appropriate for commutative function symbols, but which raises the complexity of the word problem to coNP.
References
[1]
Baader F et al. An Introduction to Description Logic 2017 Cambridge Cambridge University Press
[2]
Baader, F., Kapur, D.: Deciding the word problem for ground identities with commutative and extensional symbols. LTCS-Report 20-02, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, Dresden (2020). https://tu-dresden.de/inf/lat/reports#BaKa-LTCS-20-02
[3]
Baader F and Nipkow T Term Rewriting and All That 1998 Cambridge Cambridge University Press
[4]
Bachmair L, Ramakrishnan IV, Tiwari A, and Vigneron L Kirchner H and Ringeissen C Congruence closure modulo associativity and commutativity Frontiers of Combining Systems 2000 Heidelberg Springer 245-259
[5]
Downey P, Sethi R, and Tarjan RE Variations on the common subexpression problem J. ACM 1980 27 4 758-771
[6]
Gallier J An algorithm for finding canonical sets of ground rewrite rules in polynomial time J. ACM 1993 40 1 1-16
[7]
Kapur D Comon H Shostak’s congruence closure as completion Rewriting Techniques and Applications 1997 Heidelberg Springer 23-37
[8]
Kapur D Conditional congruence closure over uninterpreted and interpreted symbols J. Syst. Sci. Complex. 2019 32 1 317-355
[9]
Käufl T and Zabel N Stickel ME The theorem prover of the program verifier Tatzelwurm International Conference on Automated Deduction 1990 Heidelberg Springer 657-658
[10]
Kozen, D.: Complexity of finitely presented algebras. In: Proceedings of the 9th ACM Symposium on Theory of Computing, pp. 164–177. ACM (1977)
[11]
Narendran P and Rusinowitch M Book RV Any ground associative-commutative theory has a finite canonical system Rewriting Techniques and Applications 1991 Heidelberg Springer 423-434
[12]
Nelson G and Oppen DC Fast decision procedures based on congruence closure J. ACM 1980 27 4 356-364
[13]
Nieuwenhuis R and Oliveras A Fast congruence closure and extensions Inf. Comput. 2007 205 4 557-580
[14]
Schmidt RA and Waldmann U De Nivelle H Modal Tableau systems with blocking and congruence closure Automated Reasoning with Analytic Tableaux and Related Methods 2015 Cham Springer 38-53
[15]
Shostak RE An algorithm for reasoning about equality Commun. ACM 1978 21 7 583-585
[16]
Snyder W A fast algorithm for generating reduced ground rewriting systems from a set of ground equations J. Symb. Comput. 1993 15 4 415-450
[17]
Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: Proceedings of 16th Annual IEEE Symposium on Logic in Computer Science (LICS 2001), pp. 29–37. IEEE Computer Society (2001)
[18]
Wechler, W.: Universal Algebra for Computer Scientists. EATCS Monographs on Theoretical Computer Science, vol. 25. Springer, Cham (1992).
Index Terms
- Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols
Index terms have been assigned to the content through auto-classification.
Recommendations
Deciding the Word Problem for Ground and Strongly Shallow Identities w.r.t. Extensional Symbols
AbstractThe word problem for a finite set of ground identities is known to be decidable in polynomial time using congruence closure, and this is also the case if some of the function symbols are assumed to be commutative or defined by certain shallow ...
Online Recognition System for Handwritten Arabic Chemical Symbols
ICCCE '14: Proceedings of the 2014 International Conference on Computer and Communication EngineeringArabic chemical symbols are remarkably different from Latin chemical symbols which written by Arabic characters. On the other hand, Arabic chemical symbols follow Latin chemical symbols from the structure of writing the symbols. Although, Arabic symbols ...
Online Recognition System for Handwritten ARABIC Mathematical Symbols
ACSAT '13: Proceedings of the 2013 International Conference on Advanced Computer Science Applications and TechnologiesSame as Arabic scripts, Arabic mathematical symbols have some differences with Latin mathematical symbols shape. Although, Arabic Mathematical symbols follow Latin mathematical from the structure of writing the symbols, Arabic symbols have special shape ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Jul 2020
552 pages
ISBN:978-3-030-51073-2
DOI:10.1007/978-3-030-51074-9
© Springer Nature Switzerland AG 2020.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 01 July 2020
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 03 Jan 2025