Algorithmic correspondence and completeness in modal logic. II. Polyadic and hybrid extensions of the algorithm SQEMA

In Conradie, Goranko, and Vakarelov (2006, Logical Methods in Computer Science, 2) we introduced a new algorithm, SQEMA, for computing first-order equivalents and proving the canonicity of modal formulae of the basic modal language. Here we extend SQEMA, 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, 737-754) and Goranko and Vakarelov (2006, Ann. Pure. Appl. Logic, 141, 180-217), 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.