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).
  author  = {David Trachtenherz},
  title   = {Interval Temporal Logic on Natural Numbers},
  journal = {Archive of Formal Proofs},
  month   = feb,
  year    = 2011,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: List-Infinite
Used by: AutoFocus-Stream