Alexander Rabinovich - A Proof of Stavi's Theorem

lmcs:4061 - Logical Methods in Computer Science, March 6, 2018, Volume 14, Issue 1 - https://doi.org/10.23638/LMCS-14(1:20)2018
A Proof of Stavi's TheoremArticle

Authors: Alexander Rabinovich

    Kamp's theorem established the expressive equivalence of the temporal logic with Until and Since and the First-Order Monadic Logic of Order (FOMLO) over the Dedekind-complete time flows. However, this temporal logic is not expressively complete for FOMLO over the rationals. Stavi introduced two additional modalities and proved that the temporal logic with Until, Since and Stavi's modalities is expressively equivalent to FOMLO over all linear orders. We present a simple proof of Stavi's theorem.


    Volume: Volume 14, Issue 1
    Published on: March 6, 2018
    Accepted on: November 13, 2017
    Submitted on: November 13, 2017
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1236 times.
    This article's PDF has been downloaded 212 times.