Campus Event Calendar
Event Entry
What and Who
Resolution is a Decision Procedure for Many Propositional Modal Logics
Renate Schmidt
MPII
AG2 Seminar
AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, RG1, SWS
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 1 October 96
16:15
60 Minutes
46.1 - MPII
019
Saarbrücken
Abstract
The paper shows satisfiability in many propositional
modal systems, including K, KD, KT and KB, their combinations as
well as their multi-modal versions, 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 path logics.
Path logics arise from propositional and normal uni- and
multi-modal logics by the optimised functional translation
method of Ohlbach and Schmidt (1995). The decision result
provides an alternative decision proof for the relevant modal
systems. However, this alone is not very 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.
modal systems, including K, KD, KT and KB, their combinations as
well as their multi-modal versions, 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 path logics.
Path logics arise from propositional and normal uni- and
multi-modal logics by the optimised functional translation
method of Ohlbach and Schmidt (1995). The decision result
provides an alternative decision proof for the relevant modal
systems. However, this alone is not very 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.
Contact
--email hidden
passcode not visible
logged in users only