非表示:
キーワード:
-
要旨:
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.
