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

View all 14 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
44 ( #39,204 of 45,291 )

Recent downloads (6 months)
17 ( #36,479 of 45,291 )

How can I increase my downloads?

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