Sahlqvist theorem for modal fixed point logic

9Citations
Citations of this article
9Readers
Mendeley users who have this article in their library.

Abstract

We define Sahlqvist fixed point formulas. By extending the technique of Sambin and Vaccaro we show that (1) for each Sahlqvist fixed point formula φ there exists an LFP-formula χ(φ), with no free first-order variable or predicate symbol, such that a descriptive μ-frame (an order-topological structure that admits topological interpretations of least fixed point operators as intersections of clopen pre-fixed points) validates φ iff χ(φ) is true in this structure, and (2) every modal fixed point logic axiomatized by a set Φ of Sahlqvist fixed point formulas is sound and complete with respect to the class of descriptive μ-frames satisfying χ(φ): φ∈Φ. We also give some concrete examples of Sahlqvist fixed point logics and classes of descriptive μ-frames for which these logics are sound and complete. © 2011 Elsevier B.V. All rights reserved.

Cite

CITATION STYLE

APA

Bezhanishvili, N., & Hodkinson, I. (2012). Sahlqvist theorem for modal fixed point logic. Theoretical Computer Science, 424, 1–19. https://doi.org/10.1016/j.tcs.2011.11.026

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free