Journal of Logic and Computation Advance Access originally published online on September 23, 2006
Journal of Logic and Computation 2006 16(5):579-612; doi:10.1093/logcom/exl026
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||
Original Articles |
Algorithmic Correspondence and Completeness in Modal Logic. II. Polyadic and Hybrid Extensions of the Algorithm SQEMA
Department of Mathematics, University of Johannesburg and School of Mathematics, University of the Witwatersrand, Johannesburg, South Africa. E-mail: wec{at}rau.ac.za
School of Mathematics, University of the Witwatersrand, Johannesburg, South Africa.
Faculty of Mathematics and Computer Science, Sofia University, Sofia, Bulgaria. E-mail: dvak{at}fmi.uni-sofia.bg
E-mail: goranko{at}maths.wits.ac.za
In Conradie, Goranko, and Vakarelov (2006, Logical Methods in Computer Science, 2) we introduced a new algorithm,
, for computing first-order equivalents and proving the canonicity of modal formulae of the basic modal language. Here we extend
, first to arbitrary and reversive polyadic modal languages, and then to hybrid polyadic languages too. We present the algorithm, illustrate it with some examples, and prove its correctness with respect to local equivalence of the input and output formulae, its completeness with respect to the polyadic inductive formulae introduced in Goranko and Vakarelov (2001, J. Logic. Comput., 11, 737754) and Goranko and Vakarelov (2006, Ann. Pure. Appl. Logic, 141, 180217), and the d-persistence (with respect to descriptive frames) of the formulae on which the algorithm succeeds. These results readily expand to completeness with respect to hybrid inductive polyadic formulae and di-persistence (with respect to discrete frames) in hybrid reversive polyadic languages.
Keywords: Algorithm SQEMA; polyadic modal logic; hybrid logic; first-order correspondence; canonicity; completeness