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

作者：Conradie Willem^*; Goranko Valentin; Vakarelov Dimitar

来源：Journal of Applied Logic, 2010, 8(4): 319-333.

DOI：10.1016/j.jal.2010.08.002

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

The previously introduced algorithm SQEMA computes first-order frame equivalents for modal formulae and also proves their canonicity. Here we extend SOEMA 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 mu. 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.

• 出版日期2010-12