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

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-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 languageEnglish
Title of host publication9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
EditorsJakob Rehof
Place of PublicationDagstuhl, Germany
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages16:1-16:18
ISBN (electronic)9783959773232
Publication statusPublished - Jul 2024
Peer-reviewedYes

Publication series

SeriesLeibniz international proceedings in informatics : LIPIcs
Volume299
ISSN1868-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