Completeness for flat modal fixpoint logics

被引:17
|
作者
Santocanale, Luigi [2 ]
Venema, Yde [1 ]
机构
[1] Univ Amsterdam, Inst Log Language & Computat, NL-1098 XH Amsterdam, Netherlands
[2] Univ Aix Marseille 1, Lab Informat Fondamentale Marseille, F-13453 Marseille 13, France
关键词
Fixpoint logic; Modal logic; Axiomatization; Completeness; Modal algebra; Representation theorem; ALGEBRAS;
D O I
10.1016/j.apal.2010.07.003
中图分类号
O29 [应用数学];
学科分类号
070104 ;
摘要
This paper exhibits a general and uniform method to prove axiomatic completeness for certain modal fixpoint logics. Given a set Gamma of modal formulas of the form gamma(chi, p(1), ..., p(n)), where chi occurs only positively in gamma, we obtain the flat modal fixpoint language L-#(Gamma) by adding to the language of polymodal logic a connective #(gamma) for each gamma is an element of Gamma. The term #(gamma) (phi(1), ..., phi(n)) is meant to be interpreted as the least fixed point of the functional interpretation of the term gamma(chi, phi(1), ..., phi(n)). We consider the following problem: given Gamma, construct an axiom system which is sound and complete with respect to the concrete interpretation of the language L-#(Gamma) on Kripke structures. We prove two results that solve this problem. First, let K-#(Gamma) be the logic obtained from the basic polymodal K by adding a Kozen-Park style fixpoint axiom and a least fixpoint rule, for each fixpoint connective #(gamma). Provided that each indexing formula gamma satisfies a certain syntactic criterion, we prove this axiom system to be complete. Second, addressing the general case, we prove the soundness and completeness of an extension K-#(+) (Gamma) of K-#(Gamma). This extension is obtained via an effective procedure that, given an indexing formula gamma as input, returns a finite set of axioms and derivation rules for #(gamma), of size bounded by the length of gamma. Thus the axiom system K-#(+) (Gamma) is finite whenever Gamma is finite. (C) 2010 Elsevier B.V. All rights reserved.
引用
收藏
页码:55 / 82
页数:28
相关论文
共 50 条
  • [41] DEFINABILITY AND INTERPOLATION WITHIN DECIDABLE FIXPOINT LOGICS
    Benedikt, Michael
    Bourhis, Pierre
    Vanden Boom, Michael
    LOGICAL METHODS IN COMPUTER SCIENCE, 2019, 15 (03)
  • [42] COMPLETENESS IN CARDINALITY LOGICS
    JENSEN, FV
    BULLETIN DE L ACADEMIE POLONAISE DES SCIENCES-SERIE DES SCIENCES MATHEMATIQUES ASTRONOMIQUES ET PHYSIQUES, 1975, 23 (02): : 117 - 122
  • [44] KRIPKE COMPLETENESS OF STRICTLY POSITIVE MODAL LOGICS OVER MEET-SEMILATTICES WITH OPERATORS
    Kikot, Stanislav
    Kurucz, Agi
    Tanaka, Yoshihito
    Wolter, Frank
    Zakharyaschev, Michael
    JOURNAL OF SYMBOLIC LOGIC, 2019, 84 (02) : 533 - 588
  • [45] Logical data expiration for fixpoint extensions of temporal logics
    Toman, D
    ADVANCES IN SPATIAL AND TEMPORAL DATABASES, PROCEEDINGS, 2003, 2750 : 380 - 393
  • [46] On natural deduction in first-order fixpoint logics
    Szalas, Andrzej
    Fundamenta Informaticae, 1996, 26 (01) : 81 - 94
  • [47] CUT-FREE COMPLETENESS FOR MODULAR HYPERSEQUENT CALCULI FOR MODAL LOGICS K, T, AND D
    Burns, Samara
    Zach, Richard
    REVIEW OF SYMBOLIC LOGIC, 2021, 14 (04): : 910 - 929
  • [48] Completeness results for memory logics
    Areces, Carlos
    Figueira, Santiago
    Mera, Sergio
    ANNALS OF PURE AND APPLIED LOGIC, 2012, 163 (07) : 961 - 972
  • [49] Probabilization of Logics: Completeness and Decidability
    Baltazar, Pedro
    LOGICA UNIVERSALIS, 2013, 7 (04) : 403 - 440
  • [50] Completeness Results for Memory Logics
    Areces, Carlos
    Figueira, Santiago
    Mera, Sergio
    LOGICAL FOUNDATIONS OF COMPUTER SCIENCE, 2009, 5407 : 16 - +