Term rewriting systems (TRSs) are widely applied in automated theorem proving, equational languages, logic programming, specification of software and hardware, and other symbolic computations. An important computation procedure in applications of TRSs is to reduce a term to its normal form. The research of this thesis examines the complexity of normal form computation and explores efficient rewriting strategies for it.
A rewriting strategy is said optimal if for any term, it always generates the shortest derivation when computing the term's normal form. First, we prove that a universal optimal rewriting strategy for any canonical TRS does not exist unless NP=P. We prove the same result for AC TRS in which some functions are associative and commutative.
To find efficient rewriting strategies, we divide TRSs into three categories: variable-more, variable-equal, and variable-fewer, and propose optimal rewriting strategies for the first two categories and approximate strategies for the last.
We have done experiments on RRL (Rewrite Rule Laboratory) -- an automated theorem prover with term rewriting as the basic inference rule. The experiment output confirm our theoretical results. Based on our theory and experiment results, we improve RRL by implementing new programs that automatically choose an efficient rewriting strategy for an given term rewriting system.