# Interval Temporal Logic on Natural Numbers

 Title: Interval Temporal Logic on Natural Numbers Author: David Trachtenherz Submission date: 2011-02-23 Abstract: We introduce a theory of temporal logic operators using sets of natural numbers as time domain, formalized in a shallow embedding manner. The theory comprises special natural intervals (theory IL_Interval: open and closed intervals, continuous and modulo intervals, interval traversing results), operators for shifting intervals to left/right on the number axis as well as expanding/contracting intervals by constant factors (theory IL_IntervalOperators.thy), and ultimately definitions and results for unary and binary temporal operators on arbitrary natural sets (theory IL_TemporalOperators). BibTeX: @article{Nat-Interval-Logic-AFP, author = {David Trachtenherz}, title = {Interval Temporal Logic on Natural Numbers}, journal = {Archive of Formal Proofs}, month = feb, year = 2011, note = {\url{https://isa-afp.org/entries/Nat-Interval-Logic.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: List-Infinite Used by: AutoFocus-Stream