@INPROCEEDINGS{Schmidt98c,
AUTHOR = {Schmidt, R. A.},
YEAR = {1998},
TITLE = {{$E$}-Unification for Subsystems of {S4}},
EDITOR = {Nipkow, T.},
BOOKTITLE = {Rewriting Techniques and Applications: 9th International Conference, RTA'98, Proceedings},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Tsukuba, Japan},
VOLUME = {1379},
PAGES = {106--120},
NOTE = {The long version is available as Research Report
MPI-I-98-2-003, Max-Planck-Institut f{\"u}r Informatik, Saarbr{\"u}cken,
Germany.},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/Schmidt98c.html},
ABSTRACT = {This paper is concerned with the unification problem in the
path logics associated by the optimised functional translation method
with the propositional modal logics \textit{K}, \textit{KD},
\textit{KT}, \textit{KD4}, \textit{S4} and \textit{S5}.
It presents improved unification algorithms for certain forms of the
right identity and associativity laws.
The algorithms employ mutation rules, which have
the advantage that terms are worked off from the outside inward,
making paramodulating into terms superfluous.},
}