- AutorIn
- Franz Baader Technische Universität Dresden, Fakultät Informatik, Institut für Theoretische Informatik, Germany
- Deepak KapurDepartment of Computer Science, University of New Mexico, Albuquerque, USA
- Titel
- Deciding the Word Problem for Ground and Strongly Shallow Identities w.r.t. Extensional Symbols
- Zitierfähige Url:
- https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-887113
- Quellenangabe
- Journal of automated reasoning Jahrgang: 66
Seiten: 301-329
ISSN: 0168-7433
E-ISSN: 1573-0670 - Erstveröffentlichung
- 2022
- Abstract (EN)
- The 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 identities, called strongly shallow. We show that decidability in P is preserved if we add the assumption that certain function symbols f are extensional in the sense that f (s₁, . . . , sn) ≈ f (t₁, . . . , tn) implies s₁ ≈ t₁, . . . , sn ≈ tn. 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.
- Andere Ausgabe
- Link zum Artikel, der zuerst in der Zeitschrift „ Journal of automated reasoning” erschienen ist.
DOI: 10.1007/s10817-022-09624-4 - Freie Schlagwörter (DE)
- Wörterproblem für Grundidentitäten, Semantischer Kongruenzschluss, Interpretierte Funktionssymbole, Extensionalität, Ordnungsgemäße Neuschreibung
- Freie Schlagwörter (EN)
- Word problem for ground identities, Semantic congruence closure, Interpreted function symbols, Extensionality, Ordered Rewriting
- Klassifikation (DDC)
- 004
- Verlag
- Springer Science + Business Media B.V., Dordrecht [u.a.]
- Förder- / Projektangaben
- Deutsche Forschungsgemeinschaft (DFG)
Transregios TRR 248: Grundlagen verständlicher Software-Systeme - für eine nachvollziehbare cyber-physische Welt
ID: 389792660 - National Science Foundation (NSF)
Directorate for Computer & Information Science & Engineering | Division of Computing and Communication Foundations
AF: Small: Comprehensive Groebner, Parametric GCD Computations and Real Geometric Reasoning
ID: 1908804 - Version / Begutachtungsstatus
- publizierte Version / Verlagsversion
- URN Qucosa
- urn:nbn:de:bsz:14-qucosa2-887113
- Veröffentlichungsdatum Qucosa
- 22.02.2024
- Dokumenttyp
- Artikel
- Sprache des Dokumentes
- Englisch
- Lizenz / Rechtehinweis
- CC BY 4.0