[Iris-Club] Intention of later(False) in timeless predicate
jeehoon.kang at sf.snu.ac.kr
Mon Aug 22 07:00:17 CEST 2016
Dear Iris Club,
In the Iris 2.0 documentation, the timeless predicate is defined as follows
Γ |- timeless(P) <=> Γ | later(P) |- P ∨ later(False)
I guess the intention of the later(False) disjunct is allowing more
predicates to be timeless. But I am not sure which rule of "Laws for the
later modality" (page 14) requires the later(False) disjunct. May I ask is
it really used?
Jeehoon Kang (Ph.D. student) <http://sf.snu.ac.kr/jeehoon.kang>
Software Foundations Laboratory <http://sf.snu.ac.kr>
Seoul National University <http://www.snu.ac.kr>
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Iris-Club