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
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.