E-Unification for Subsystems of S4

Schmidt, Renate A.

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

E-Unification for Subsystems of S4

MPS-Authors

/persons/resource/persons45401

Schmidt, Renate A.
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

Schmidt, R. A. (1998). E-Unification for Subsystems of S4. In T. Nipkow (Ed.), Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98) (pp. 106-120). Berlin, Germany: Springer.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-3834-2

Abstract

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