Small Term Reachability and Related Problems for Terminating Term Rewriting Systems

Franz Baader, Jürgen Giesl

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 t…