| |
VOLUME 2, ISSUE 1, PAPER 5
|
Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
|
©Willem Conradie, University of Johannesburg
©Valentin Goranko, University of the Witwatersrand
©Dimiter Vakarelov, Sofia University
|
Abstract
Modal formulae express monadic second-order properties on Kripke
frames, but in many important cases these have first-order
equivalents. Computing such equivalents is important for both logical
and computational reasons. On the other hand, canonicity of modal
formulae is important, too, because it implies frame-completeness of
logics axiomatized with canonical formulae.
Computing a first-order equivalent of a modal formula amounts to
elimination of second-order quantifiers. Two algorithms have been
developed for second-order quantifier elimination: SCAN, based on
constraint resolution, and DLS, based on a logical equivalence
established by Ackermann.
In this paper we introduce a new algorithm, SQEMA, for computing
first-order equivalents (using a modal version of Ackermann's lemma)
and, moreover, for proving canonicity of modal formulae. Unlike SCAN
and DLS, it works directly on modal formulae, thus avoiding
Skolemization and the subsequent problem of unskolemization. We
present the core algorithm and illustrate it with some examples. We
then prove its correctness and the canonicity of all formulae on which
the algorithm succeeds. We show that it succeeds not only on all
Sahlqvist formulae, but also on the larger class of inductive
formulae, introduced in our earlier papers. Thus, we develop a purely
algorithmic approach to proving canonical completeness in modal logic
and, in particular, establish one of the most general completeness
results in modal logic so far.
|
Publication date: March 7, 2006
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-2(1:5)2006
Hit Counts: 5072 |
 Creative Commons | |
