Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Zeitschriftenartikel

Decidability by Resolution for Propositional Modal Logics

MPG-Autoren
/persons/resource/persons45401

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

Externe Ressourcen
Es sind keine externen Ressourcen hinterlegt
Volltexte (beschränkter Zugriff)
Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte in PuRe verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Schmidt, R. A. (1999). Decidability by Resolution for Propositional Modal Logics. Journal of Automated Reasoning, 22(4), 379-396.


Zitierlink: https://hdl.handle.net/11858/00-001M-0000-000F-363E-9
Zusammenfassung
The paper shows that satisfiability in a range of popular propositional modal systems can be decided by ordinary resolution procedures. This follows from a general result that resolution combined with condensing, and possibly some additional form of normalisation, is a decision procedure for the satisfiability problem in certain so-called path logics. Path logics arise from normal propositional modal logics by the optimised functional translation method. The decision result provides an alternative method of proving decidability for modal logics, as well as closely related systems of artificial intelligence. This alone is not interesting. A more far-reaching consequence of the result has practical value, namely, any fair implementation of a first-order theorem prover which is based on resolution is suitable for facilitating modal reasoning.