E-unification for subsystems of S4

Schmidt, Renate A.

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Report

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)

MPI-I-98-2-003.pdf
(Any fulltext), 353KB

Supplementary Material (public)

There is no public supplementary material available

Citation

Schmidt, R. A.(1998). E-unification for subsystems of S4 (MPI-I-1998-2-003). Saarbrücken: Max-Planck-Institut für Informatik.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-7B54-1

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.