Algorithmic correspondence and completeness in modal logic. V. Recursive extensions of SQEMA

Willem Conradie, Valentin Goranko, Dimiter Vakarelov

    Research output: Contribution to journalJournal articleResearchpeer-review

    Abstract

    The previously introduced algorithm SQEMA computes first-order frame equivalents for modal formulae and also proves their canonicity. Here we extend SQEMA with an additional rule based on a recursive version of Ackermann's lemma, which enables the algorithm to compute local frame equivalents of modal formulae in the extension of first-order logic with monadic least fixed-points FOμ. This computation operates by transforming input formulae into locally frame equivalent ones in the pure fragment of the hybrid μ-calculus. In particular, we prove that the recursive extension of SQEMA succeeds on the class of ‘recursive formulae’. We also show that a certain version of this algorithm guarantees the canonicity of the formulae on which it succeeds.
    Original languageEnglish
    JournalJournal of Applied Logic
    Volume8
    Issue number4
    Pages (from-to)319-333
    ISSN1570-8683
    DOIs
    Publication statusPublished - 2010

    Keywords

    • Correspondence theory
    • Canonicity
    • Modal logic
    • First-order logic with fixed-points
    • SQEMA

    Fingerprint Dive into the research topics of 'Algorithmic correspondence and completeness in modal logic. V. Recursive extensions of SQEMA'. Together they form a unique fingerprint.

    Cite this