На 29 март 2024 г. (петък) от 13:00 часа ще се проведе дистанционно заседание на семинара по „Алгебра и логика”.

Доклад на тема:

Generalized Definability of Discrete Time Interval-based Temporal Connectives

ще изнесе

Димитър Гелев, ИМИ – БАН.

Абстракт. 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 #(A₁,…,A_m) can be produced that is built from the past, future and introspective formulas appearing in some separated equivalents of the operands A₁,…,A_m. 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.

Линк към Zoom-стаята на семинара:
https://us02web.zoom.us/j/85137375021?pwd=RE5QczdFTE1xL1R6MnI2b1lkcGczQT09