It is proposed to investigate term rewriting systems and mechanical theoremproving strategies. The topics to be studied include: polynomial timealgorithms for reducing ground term rewriting systems to canonical form, andtheir application to the rigid E.unification problem; semantics and confluencetests for conditional term rewriting systems; and the use of rewriting andunification in programming languages. The research has potential applicationsin program verification and automated reasoning.
