The next meeting of the Algebra and Logic Seminar will be held online via Zoom on March 29, 2024 (Friday) at 1:00 pm (UTC+2).
A talk on:
Generalized Definability of Discrete Time Interval-based Temporal Connectives
will be delivered by
Dimitar Guelev (Institute of Mathematics and Informatics, Bulgarian Academy of Sciences).
Abstract.In Linear Temporal Logic with past (PLTL), expressive completeness implies that any first-order definable connective is also definable in the temporal language based on the Since and Until temporal operators. This is not the case about discrete time interval-based temporal logics with state-based semantics for the propositional variables. In this talk I prove the next best thing about the extension ITLNL of Moszkowski’s discrete time propositional Interval Temporal Logic (ITL) by the neighbourhood modalities: given an interval-based connective # which admits a first-order definition, a star-free ITLNL defining formula for #(A1,…,Am) can be produced that is built from the past, future and introspective formulas appearing in some separated equivalents of the operands A1,…,Am. The proof is based in an interval-based analogue of Gabbay’s separation theorem about PLTL that was previously established about ITLNL by the neighbourhood modalities by me and Moszkowski and have now used to prove the expressive completeness of ITLNL. As a side result I have come upon new proofs of expressive completeness and temporal separation for ITLNL’s star-free subset that I will briefly discuss too.
Link to the Zoom room:
https://us02web.zoom.us/j/
Algebra and Logic Department, IMI – BAS
http://www.math.bas.bg/algebra/seminarAiL/
============================== =====================