MPI-I-98-2-003

E-unification for subsystems of S4

Schmidt, Renate A.

MPI-I-98-2-003. April 1998, 30 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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.
Acknowledgement:
References to related material:

To download this research report, please select the type of document that fits best your needs.	Attachement Size(s):
	383 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView

URL to this document: http://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},}