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

Affordable Access

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

Authors
Publisher
Elsevier BV
Keywords
  • Sqema
  • Modal Logic
  • Correspondence Theory
  • Canonicity
  • First-Order Logic With Fixed-Points

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 FOμ. This computation operates by transforming input formulae into locally frame equivalent ones in the pure fragment of the hybrid μ-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.

There are no comments yet on this publication. Be the first to share your thoughts.