Affiliations: Department of Mathematics, University of Johannesburg,
Johannesburg, South Africa. [email protected] | Department of Informatics and Mathematical Modelling,
Technical University of Denmark, Germany. [email protected] | Faculty of Mathematics and Computer Science, Sofia
University, Sofia, Bulgaria. [email protected]
Note: [] Address for correspondence: Faculty of Mathematics and Computer
Science, Sofia University, Sofia, Bulgaria
Abstract: In earlier papers we have introduced an algorithm, SQEMA, for
computing first-order equivalents and proving canonicity of modal formulae.
However, SQEMA is not complete with respect to the so called complex Sahlqvist
formulae. In this paper we, first, introduce the class of complex inductive
formulae, which extends both the class of complex Sahlqvist formulae and the
class of polyadic inductive formulae, and second, extend SQEMA to SQEMA^{sub} by
allowing suitable substitutions in the process of transformation. We prove the
correctness of SQEMA^{sub} with respect to local equivalence of the input and
output formulae and d-persistence of formulae on which the algorithm succeeds,
and show that SQEMA^{sub} is complete with respect to the class of complex
inductive formulae.
