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

Journal of Applied Logic 8 (4):319-333 (2010)
Download Edit this record How to cite View on PhilPapers
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 \mffo. This computation operates by transforming input formulae into locally frame equivalent ones in the pure fragment of the hybrid mu-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.
PhilPapers/Archive ID
Upload history
Archival date: 2018-04-20
View other versions
Added to PP index

Total views
72 ( #49,206 of 2,444,856 )

Recent downloads (6 months)
4 ( #59,989 of 2,444,856 )

How can I increase my downloads?

Downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.