hide
Free keywords:
-
Abstract:
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.
