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
Revision history
Archival date: 2018-04-20
View upload history
References found in this work BETA
Modal Logic.Blackburn, Patrick; de Rijke, Maarten & Venema, Yde
Modal Logic and Classical Logic.van Benthem, J. F. A. K.

View all 17 references / Add more references

Citations of this work BETA
Sahlqvist Correspondence for Modal Mu-Calculus.van Benthem, Johan; Bezhanishvili, Nick & Hodkinson, Ian

Add more citations

Added to PP index

Total views
56 ( #40,930 of 50,239 )

Recent downloads (6 months)
12 ( #37,860 of 50,239 )

How can I increase my downloads?

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