Abstract, BibTeX, PDF.

The most natural means for specifying a non-classical logic
is by means of a Hilbert calculus. Usually, the semantics
of a non-classical logic is given in terms of possible
worlds. Given an axiomatization of a non-classical logics,
the *correspondence problem* in these logics is to
find for every given Hilbert axiom an equivalent property
of the accessibility relation (van Benthem (1984)). For
mechanizing deduction in non-classical logics it is very
important to find these correspondences (Ohlbach (1991)).
So far the method for finding the correspondences was mostly
by intuition and the verification required complex proofs
(van Benthem (1984)). SCAN is an algorithm which offers
a method for computing the correspondences fully automatically.
Moreover, since SCAN preserves equivalences, the computed
correspondence axioms are *guaranteed to be complete*
in the sense that a formula is derivable in the Hilbert
calculus if and only if it is valid in the frames which
are models of the computed correspondence axiom. In this
paper we present the SCAN algorithm and an application
of it to the problem of collapsing modalities in multi-modal
logics: Given a Hilbert calculus for modalities [m_1]
and [m_2] we have to ensure that [m_1] P iff [m_2] P
doesn't hold for all formulae
P, because this is in general an unwanted consequence
of the given axiomatization.
[an error occurred while processing this directive]