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
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 \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
CONACA-8
Revision history
Archival date: 2018-04-20
View upload history
References found in this work BETA

View all 8 references / Add more references

Citations of this work BETA

Add more citations

Added to PP index
2016-06-30

Total views
19 ( #36,008 of 38,678 )

Recent downloads (6 months)
9 ( #31,088 of 38,678 )

How can I increase my downloads?

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