================================================================================
P9505   J.M.T. Romijn
        "Automatic analysis of term rewriting systems: proving properties
        of term rewriting systems derived from ASF+SDF specifications"


Term rewriting systems are used frequently as an implementation technique
for algebraic specifications. We present a supporting tool for the ASF+SDF
Meta-environment that derives a conditional term rewriting system from an
ASF+SDF specification, and tests this system for certain properties. The
properties included are: non-erasing, orthogonal, recursive program scheme
and strongly normalizing.

Since the specification from which we derive the conditional term rewriting
system has some specific ASF+SDF features, the theory that supports this
derivation is somewhat different from well-known term rewrite theories.
To keep this supporting theory sound, not every ASF+SDF feature is allowed.

The property strongly normalizing is in general not decidable. We chose the
method of recursive path orderings to be able to prove the property for a
subset of the possible term rewriting systems.

The future ASF+SDF Meta-environment will be based on ASF+SDF specifications,
so-called meta-level specifications. Although this new Meta-environment is
not yet ready for use, the implementation of the tool presented here is
based on the future situation.