[Iris-Club] Questions on proof rules
jeehoon.kang at sf.snu.ac.kr
Tue Aug 23 04:33:10 CEST 2016
Dear Iris Club,
I have several questions on the proof rules in the Iris 2.0 documentation.
- (Section 5.3) in the rule for deriving timeless(V(a)), I think the
premise is not sufficient (a is a discrete COFE element). I think we need
more information on V to derive the conclusion.. May I ask how do you
prove the soundness of this rule?
- (Section 5.3) I think in general P * Q |- P /\ Q holds from the model.
If so, the following rules for the always modality seems redundant:
+ always(P * Q) |- always(P /\ Q)
+ always(P) * Q |- always(P) /\ Q
How do you consider this argument?
- (Section 7.1) I think there is a typo in the 3rd rule: should it be on
the universal quantification?
- (Section 7.1) I am not sure how to derive the 4th rule from the rules in
PS. I want to say thank you all for all the answers you all have replied.
I just didn't have a chance to say that because I did not want to send too
much email :-)
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