Justification announcements in discrete time. Part II: Frame\n definability results

2017/08/21 by Grigory K. Olkhovikov, Olkhovikov, Grigory K.
Computer Science · #FOS: Mathematics #Formal Methods in Verification #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.1708.06295

openalex publication_date 2017/08/21 · openalex created_date 2022/10/07 · openalex updated_date 2026/07/28

Abstract

In Part I of this paper, we presented a Hilbert-style system \Σ_D\naxiomatizing of stit logic of justification announcements (JA-STIT) interpreted\nover models with discrete time structure. In this part, we prove three frame\ndefinability results for \Σ_D using three different definitions of a\nframe plus a yet another version of completeness result.\n

Related

• Stit logic of justification announcements: a completeness result
• Explicit justification stit logic: a completeness result
• A Fast Algorithm and Datalog Inexpressibility for Temporal Reasoning
• Appendix for: Cut-free Calculi and Relational Semantics for Temporal STIT logics
• Public Announcement Logic in Geometric Frameworks