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{http://isa-afp.org/entries/Nat-Interval-Logic.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: List-Infinite
Used by: AutoFocus-Stream