On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
Contributors
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
| Original language | English |
|---|---|
| Title of host publication | 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024) |
| Editors | Jakob Rehof |
| Place of Publication | Dagstuhl, Germany |
| Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
| Pages | 16:1-16:18 |
| ISBN (electronic) | 9783959773232 |
| Publication status | Published - Jul 2024 |
| Peer-reviewed | Yes |
Publication series
| Series | Leibniz international proceedings in informatics : LIPIcs |
|---|---|
| Volume | 299 |
| ISSN | 1868-8969 |
External IDs
| Scopus | 85198827616 |
|---|---|
| ORCID | /0000-0002-4049-221X/work/174429060 |
Keywords
ASJC Scopus subject areas
Keywords
- Confluence, Creating small terms, Derivational complexity, Description Logics, Proof rewriting, Rewriting, Termination