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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Wed, 3 May 2017 14:30:23 +0200*References*: <CAOcQdOWHqNaDV9OcPw0Mey3+2pXBobtJB37+TMrg5b3rzzEAUA@mail.gmail.com>

Hello, > On 3 May 2017, at 10:46, kacem belout <belout...@xxxxxxxxx> wrote: > > Hallo, > > I noticed the following theorems concerning the ENABLED Operator that I hopefully would like to prove them in a formal way ( i.e Formally ( Logically and/or symbolically) as using Inference Rules) as I tried to explain before, in order to give a precise meaning to your notion of "formal" proof, you would need to give clear definitions. > > In the context of the Raw Logic (RTLA), for any Action A, we assert the following valid statements. I don't understand why you insist on Raw TLA: the difference between RTLA and TLA only exists at the temporal level, and you don't consider any temporal formulas. Also, it would help if you used actual TLA syntax. > Let me know if any one is not valid by giving a counterexample, thanks !. > > Theorem 1 : A ==> ENABLED(A) > Proof : Now, I don't know How To formally and mechanically derive ENABLED(A) From A which is expressed in terms of primed variables and unprimed variables. See my previous answer: the implication holds for the same reason why F => \E X: F is a theorem of first-order logic. > > Theorem 2 : \Not ENABLED(A) ==> \Not A > Proof : Is equivalent to Theorm1 by propositional logic rule (implication equivalente to its contrapositive). Yes, so it's just a corollary to the previous theorem. > > Theorem 3 : \Not A ==> \Not ENABLED(A) Wrong. Consider A == x = 0 /\ x' = 1 and a state s that assigns 0 to x. Then the stuttering step (s,s) satisfies ~ A and ENABLED A. > > Theorem 4 : \Not (ENABLED(A)) ==> ENABLED( \Not (A)) Consequence of Theorems 1 and 2. > > Theorem 5 : ENABLED(A) <==> ENABLED(-1(A)) , where -1(A) == (A)-1 ; inverse of A. (A)-1 == A ( v ' <- v , v <- v ') Wrong, take again A == x=0 /\ x'=1. then ENABLED A \equiv x = 0 ENABLED (A)-1 \equiv x = 1 > > Theorem 6 : For any state predicate P. P <==> ENABLED(P) Correct. > Theorem 7 : For any state predicate P. P ==> ENABLED((P) '), where ' == Prime operator. Correct. (ENABLED P' is true iff P is satisfiable.) > Theorem 8 : For any state predicate P. P ==> ENABLED(((p)')-1) Isn't (P')-1 = P, so this is the same as theorem 6? Regards, Stephan

**References**:**ENABLED Operator Theorems***From:*kacem belout

- Prev by Date:
**ENABLED Operator Theorems** - Next by Date:
**TLA+ Toolbox 1.5.3 not displaying error trace** - Previous by thread:
**ENABLED Operator Theorems** - Next by thread:
**TLA+ Toolbox 1.5.3 not displaying error trace** - Index(es):