SQEMA

an algorithm for computing first-order correspondences in modal logic: an implementation Dimiter Georgiev, Tinko Tinchev and Dimiter Vakarelov Sofia University

The first implemented algorithms in this field are the algorithm SCAN introduced by Gabbay and Ohlbach in [6] and the algorithm DLS originated by Szalas [8] (see more on these algorithms in [7]). SCAN is based on a resolution procedure applied on a Skolemized translation of the modal formula into the first-order logic, while DLS works on the same translation, but is based on a transformation procedure using a lemma by Ackermann. Both algorithms use a procedure of unskolemization, which is not always successful. In [2] and [3] another algorithm for computing first-order correspondents for modal formulas was introduced, called SQEMA, which is based on a modal version of the Ackermann lemma. The algorithm works directly on the modal formulas without translating them into a first-order logic and without using Scolemization. SQEMA suceeds not only on all Sahlqvist formula, but also on the extended class of inductive formulas introduced in [4]. Furthermore, there are examples of modal formulas on which SQEMA suceeds, while both SCAN and DLS fail, e.g.:
((p <-> q) -> p)
Here is another interesting example, that is supported in the implementation of SQEMA, courtesy of Renate Schmidt:
((p -> p) (p -> p))
On the other hand, we are interested in examples of first-order definable modal formulas on which SCAN or DLS succeeds but SQEMA fails. If anyone finds such examples, pease send them to the webmaster. A most important feature of SQEMA is that, as proved in [2] and [3], it only succeeds on canonical (d-persistent) formulas, i.e., whenever successful, it not only computes a local first-order correspondent of the input modal formula, but also proves its canonicity and therefore the canonical completeness of the modal logic axiomatized with that formula. This accordingly extends to any finite set of modal formulas on which SQEMA suceeds. Thus, SQEMA can also be used as an automated prover of canonical model completeness of modal logics.
An implementation in Java of SQEMA was given in [1]. It supports nominals in the input and, as output, it gives a nominal formula and its translation into a first-order formula. Some simplifications of the first-order formula are also implemented.
An extension of SQEMA, SQEMA+U, was presented at the 10th Panhellenic Logic Symposium. The slides and the abstract are available.

REFERENCES
[1] Georgiev, Dimiter. An implementation of the algorithm SQEMA for computing first-order correspondences of modal formulas. Master thesis. Sofia University, Faculty of mathematics and computer science, 2006.
[2] Conradie, W., V. Goranko and D. Vakarelov. Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA, Logical Methods in Computer Science, vol. 2 (1:5) 2006, pp.1-26. Available from http://www.lmcs-online.org/ojs/viewarticle.php?id=127&layout=abstract
[3] Conradie, W., V. Goranko and D. Vakarelov. Algorithmic correspondence and completeness in modal logic II. Polyadic and hybrid extensions of the algorithm SQEMA. 2006. Submitted.
[4] V. Goranko and D. Vakarelov. Elementary Canonical Formulae: Extending Sahlqvist Theorem, Annals of Pure and Applied Logics, 2006, vol. 141, 1-2, pp. 180-217. Link: http://dx.doi.org/10.1016/j.apal.2005.10.005 .
[5] Conradie, W., V. Goranko and D. Vakarelov. Elementary Canonical Formulae: a survey on syntactic, algorithmic, and model-theoretic aspects, in: Advances in Modal Logic, vol. 5, Kings College London Publ., 2005, pp. 17-51. Link: http://www.aiml.net/volumes/volume5/
[6] Gabbay, D. and Ohlbach, H. Quantifier Elimination in Second-order Logic. South African Computer Journal, 7, (1992), 35?43.
[7] Nonnengart, A., H. J. Ohlbach, and A. Szalas. Quantifier elimination for second-order predicate logic, in: Logic, Language and Reasoning: Essays in honour of Dov Gabbay, Part I, H. J. Ohlbach and U. Reyle (eds.), Kluwer, 1997.
[8] A. Szalas, On the correspondence between Modal and Classical Logic: an Automated Approach. J. Logic and Comp. Vol 3 No 6(1993), 605-620.