E-Unification for Subsystems of S4

Schmidt, R. A. (1998)

In Rewriting Techniques and Applications: 9th International Conference, RTA'98, Tsukuba, Japan, Proceedings, Nipkow, T. (ed.), Lecture Notes in Computer Science 1379, Springer, 106-120. BiBTeX, PostScript (Copyright © Springer)

This paper is concerned with the unification problem in the path logics associated by the optimised functional translation method with the modal logics K, KD, KT, KD4, S4 and 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.

The long version is Research Report MPI-I-98-2-003, Max-Planck-Institut für Informatik, Saarbrücken, Germany. BiBTeX, PostScript
Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 24 Jan 2000
Copyright © 1996,7,8 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk