On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems
Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/Gutachten › Beitrag in Konferenzband › Beigetragen › Begutachtung
Beitragende
Abstract
Motivated by an application where we try to make proofs for Description Logic inferences smaller by rewriting, we consider the following decision problem, which we call the small term reachability problem: given a term rewriting system R, a term s, and a natural number n, decide whether there is a term t of size ≤ n reachable from s using the rules of R. We investigate the complexity of this problem depending on how termination of R can be established. We show that the problem is NP-complete for length-reducing term rewriting systems. Its complexity increases to N2ExpTimecomplete (NExpTime-complete) if termination is proved using a (linear) polynomial order and to PSpace-complete for systems whose termination can be shown using a restricted class of Knuth-Bendix orders. Confluence reduces the complexity to P for the length-reducing case, but has no effect on the worst-case complexity in the other two cases.
Details
| Originalsprache | Englisch |
|---|---|
| Titel | 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024) |
| Redakteure/-innen | Jakob Rehof |
| Erscheinungsort | Dagstuhl, Germany |
| Herausgeber (Verlag) | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
| Seiten | 16:1-16:18 |
| ISBN (elektronisch) | 9783959773232 |
| Publikationsstatus | Veröffentlicht - Juli 2024 |
| Peer-Review-Status | Ja |
Publikationsreihe
| Reihe | Leibniz international proceedings in informatics : LIPIcs |
|---|---|
| Band | 299 |
| ISSN | 1868-8969 |
Externe IDs
| Scopus | 85198827616 |
|---|---|
| ORCID | /0000-0002-4049-221X/work/174429060 |
Schlagworte
ASJC Scopus Sachgebiete
Schlagwörter
- Confluence, Creating small terms, Derivational complexity, Description Logics, Proof rewriting, Rewriting, Termination