On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

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

OriginalspracheEnglisch
Titel9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Redakteure/-innenJakob Rehof
ErscheinungsortDagstuhl, Germany
Herausgeber (Verlag)Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Seiten16:1-16:18
ISBN (elektronisch)9783959773232
PublikationsstatusVeröffentlicht - Juli 2024
Peer-Review-StatusJa

Publikationsreihe

ReiheLeibniz international proceedings in informatics : LIPIcs
Band299
ISSN1868-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