MPI-INF Logo
MPI-INF/SWS Research Reports 1991-2017

2. Number - only D2

MPI-I-97-2-002

Resolution is a decision procedure for many propositional modal logics

Schmidt, Renate A.

January 1997, 60 pages.

.
Status: available - back from printing

The paper shows satisfiability in many propositional modal systems can be decided by ordinary resolution procedures. This follows from a general result that resolution and condensing is a decision procedure for the satisfiability problem of formulae in so-called \emph{path logics}. Path logics arise from propositional and normal uni- and multi-modal logics by the \emph{optimised functional translation} method. The decision result provides an alternative decision proof for the relevant modal logics (including \textit{K}, \textit{KD}, \textit{KT} and \textit{KB}, their combinations as well as their multi-modal versions), and related systems in artificial intelligence. This alone is not interesting. A more far-reaching consequence of the result has practical value, namely, any standard first-order theorem prover that is based on resolution can serve as a reasonable and efficient inference tool for modal reasoning.

  • MPI-I-97-2-002.ps
  • Attachement: ATT7G2RP (423 KBytes)

URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1997-2-002

Hide details for BibTeXBibTeX
@TECHREPORT{Schmidt97,
  AUTHOR = {Schmidt, Renate A.},
  TITLE = {Resolution is a decision procedure for many propositional modal logics},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-97-2-002},
  MONTH = {January},
  YEAR = {1997},
  ISSN = {0946-011X},
}