[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Sun, 30 Apr 2017 18:37:23 +0200*References*: <8b96dd40-4123-4cb6-a2c7-cba8e6fba8da@googlegroups.com>

Hi again, > On 30 Apr 2017, at 18:17, belout...@xxxxxxxxx wrote: > > Thanks Stephan For your rapid reply, > > You say the proof is obvious. But, I can not see How to make the Proof in a formal way of this Theorem . you have not explained what you mean by "formal" – which proof system are you thinking of? Semantically, the reasoning is as follows: ENABLED A is a state predicate that holds in state s if there exists some state t such that the pair (s,t) of states satisfies A. The implication A => ENABLED A is an action formula and as such is evaluated over a pair of states,. So take an arbitrary pair (s,t) of states. If (s,t) does not satisfy A, the implication holds trivially. If it does, then s also satisfies ENABLED A, since we know that there is a state t such that A holds of the pair (s,t). Syntactically, you need to expand ENABLED into a quantification over all flexible state variables that have (free) occurrences in A, and so the implication generalizes the standard theorem F => \E x: F of first-order logic. > > Furthermore, What about The suggested Inference Rules ? > > > A A > R1: --------------- R2:---------------- > A ==> Enabled(A) Enabled(A) > Again, without an explanation of the proof system in which these rules are stated I cannot really know their intended meaning. In particular, should I read a premise "A" in a proof rule as asserting that A is true of an arbitrary pair of states? This would be a standard interpretation of proof rules in modal logic but would make rule R2 pretty useless. As for R1, since the consequent is already a theorem, the premise is unnecessary. Have you read some formal exposition of the logic TLA [1,2]? Hope this helps, Stephan [1] L. Lamport. The Temporal Logic of Actions. TOPLAS 16(3):872-923, 1994. [2] S. Merz. The specification language TLA+. In: Logics of Specification Languages (D. Bjørner, M.C. Henson, eds.), Monographs in Theoretical Computer Science, pp. 401-451, 2008. > Thanks For Help > > > > -- > You received this message because you are subscribed to the Google Groups "tlaplus" group. > To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx. > To post to this group, send email to tla...@xxxxxxxxxxxxxxxx. > Visit this group at https://groups.google.com/group/tlaplus. > For more options, visit https://groups.google.com/d/optout.

**References**:**Quest. Cont. About Theorem And Inference Rule***From:*belout . . .

- Prev by Date:
**Quest. Cont. About Theorem And Inference Rule** - Next by Date:
**Leibniz and ToBoolean Operators and Proof Fragment** - Previous by thread:
**Quest. Cont. About Theorem And Inference Rule** - Next by thread:
**Leibniz and ToBoolean Operators and Proof Fragment** - Index(es):