Name
Title | ||
|---|---|---|
Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols. |
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 \(f(s_1,\ldots ,s_n) \mathrel {\approx }f(t_1,\ldots ,t_n)\) implies \(s_1 \mathrel {\approx }t_1,\ldots ,s_n \mathrel {\approx }t_n\). 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. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.1007/978-3-030-51074-9_10 | IJCAR (1) |
Keywords | DocType | Citations |
Word problem (mathematics),Commutative property,Extensionality,Decidability,Finite set,Combinatorics,Time complexity,Approx,Mathematics,Extensional definition | Conference | 0 |
PageRank | References | Authors |
0.34 | 0 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Franz Baader | 1 | 8123 | 646.64 |
| Deepak Kapur | 2 | 0 | 2.37 |