MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments


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: (383 KBytes)

URL to this document:

Hide details for BibTeXBibTeX
  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},