MPI-I-98-2-003
E-unification for subsystems of S4
Schmidt, Renate A.
April 1998, 30 pages.
.
Status: available - back from printing
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.
-
- Attachement: MPI-I-98-2-003.ps (383 KBytes)
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1998-2-003
BibTeX
@TECHREPORT{Schmidt98,
AUTHOR = {Schmidt, Renate A.},
TITLE = {E-unification for subsystems of S4},
TYPE = {Research Report},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
NUMBER = {MPI-I-98-2-003},
MONTH = {April},
YEAR = {1998},
ISSN = {0946-011X},
}