Projekt A9 
Die Sprache der grundreduzierbaren Terme
(The language of ground reducible terms)
(until December 2003)
This project is an extension of Project A6.
There we especially obtained interesting results for the language
of ground reducible terms in case only linear terms are considered
and the left hand sides of the underlying term rewriting system are
linear as well
(a term is called linear if no variable occurs twice in it):

We showed that the language of linear terms ground reducible w.r.t.
a leftlinear term rewriting system is regular.

We gave a characterization of finite and uniform test sets
for deciding ground reducibility of linear terms w.r.t. a
leftlinear term rewriting system through congruence relations and
tree automata. (Uniform here means that the test set only depends
on the rewrite system and not on the terms that are checked for
ground reducibility.)

This on the one side led to effective construction of minimal
test sets. On the other side it brought together
the two competing approaches to ground reducibility 
the test set and the automaton approach. In this way it helped
us to a better understanding of both.
Now our focus is on arbitrary (nonlinear) term rewriting systems
and we investigate the following questions:

How to classify the language of (linear) ground reducible terms?

Is there an effective characterization of finite and uniform
test sets for ground reducibility?
Here we have to deal with more complex language classes:
Whereas for leftlinear term rewriting systems
the language of reducible ground terms constitutes a regular
tree language, for arbitrary term rewriting systems a language
accepted by a constrained automaton is obtained, since we have
to keep track of equalities between subterms. Consequently
appropriate test sets also become rather complex, as already
pointed out in our article on linearisation of term rewriting systems.
Members:
Dieter Hofbauer
Maria Huber
Technical Reports:

Hofbauer, D. and Huber, M.:

Test Sets for the Universal and Existential Closure of Regular Tree Languages.
Mathematische Schriften Kassel 7/99,
UniversitätGH Kassel (42 pages), October 1999.
(To appear in Information and Computation.)
Publications:

Hofbauer, D. and Huber, M.:

Test Sets for the Universal and Existential Closure of Regular Tree Languages.
Proc. of the 10th International Conference on Rewriting Techniques and Applications,
RTA 99, Trento (Italy),
Lecture Notes in Computer Science 1631, pages 205219, 1999.

Hofbauer, D. and Huber, M.:

Linearizing Term Rewriting Systems using Test Sets.
Journal of Symbolic Computation
17, pp. 91129, 1994.