[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Quest. Cont. About Theorem And Inference Rule
> 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,
 L. Lamport. The Temporal Logic of Actions. TOPLAS 16(3):872-923, 1994.
 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.