de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Impressum Kontakt Einloggen
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Bericht

Resolution is a decision procedure for many propositional modal logics

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45401

Schmidt,  Renate A.
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)

1997-2-002
(beliebiger Volltext), 10KB

Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Schmidt, R. A.(1997). Resolution is a decision procedure for many propositional modal logics (MPI-I-1997-2-002). Saarbrücken: Max-Planck-Institut für Informatik.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-0014-9B9D-E
Zusammenfassung
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.