Algorithmic Correspondence and Completeness in Modal Logic. III. Extensions of the Algorithm SQEMA with Substitutions

W. Conradie, Valentin Goranko, D. Vakarelov

    Research output: Contribution to journalJournal articleResearchpeer-review

    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.
    Original languageEnglish
    JournalFundamenta Informaticae
    Volume92
    Issue number4
    Pages (from-to)307-343
    ISSN0169-2968
    DOIs
    Publication statusPublished - 2009

    Keywords

    • complex Sahlqvist formulae
    • d-persistence
    • correspondence
    • SQEMA

    Fingerprint

    Dive into the research topics of 'Algorithmic Correspondence and Completeness in Modal Logic. III. Extensions of the Algorithm SQEMA with Substitutions'. Together they form a unique fingerprint.

    Cite this