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

*From*: jack malkovick <sillymouse333@xxxxxxxxx>*Date*: Wed, 30 Nov 2022 02:09:20 -0800 (PST)*References*: <904caba2-762e-49a2-bea5-1dc6a3506929n@googlegroups.com> <498A9107-441B-4AA3-A9B1-F23E27AFAD86@gmail.com> <a244225f-f9a0-4db7-894c-cf52fd0bd762n@googlegroups.com> <1D76B0CC-53E7-4F77-83FD-96FE922D0F9C@gmail.com>

Thank you! You are right, being suspicious is a very healthy thing

On Wednesday, November 30, 2022 at 12:04:50 PM UTC+2 Stephan Merz wrote:

Hi,you discovered why verification is not a panacea. You may prove the most elaborate theorems, but they are meaningless if your specification does not represent the actual system, and an inconsistent set of assumptions is just the most extreme example. Therefore, you need to be suspicious of success and validate your spec as much as you can. Simulation, as well as model checking non-properties and examining the counter-examples are useful for that.Note that this problem applies to both model checking and theorem proving. You should get suspicious if model checking completes very quickly, finds fewer reachable states than you expect, and/or if some actions are taken only rarely or never (TLC provides statistics for this). In theorem proving, get suspicious if a proof obligation that looks complicated is solved quickly and automatically, as it may indicate a contradiction between assumptions – although this is of course not always the case.Regards,StephanOn 30 Nov 2022, at 10:11, jack malkovick <sillym...@xxxxxxxxx> wrote:Yes, it makes sense, I tried that too before...I guess I was looking for a way to formulate a theorem in such a way it will be unprovable having an inconsistent set of facts.Would that make any sense?On Wednesday, November 30, 2022 at 11:04:37 AM UTC+2 Stephan Merz wrote:Hi,could you explain why you are surprised? The theorem holds for two reasons: (i) the assertion (TRUE) is trivial, and (ii) the assumptions are contradictory, as you say. From contradictory assumptions, anything can be proved, and in fact the following also passes:THEOREM

ASSUME

NEW P(_),

\A p : P(p),

\A p : ~P(p)

PROVEFALSE

OBVIOUS

Regards,

StephanOn 30 Nov 2022, at 09:53, jack malkovick <sillym...@xxxxxxxxx> wrote:I just started reading about TLAPS and I tried for fun the followingsillythingTHEOREM T ==

ASSUME

NEW P(_),

\A p : P(p),

\A p : ~P(p)

PROVE

TRUE

PROOF

OBVIOUSTo my surprise, the result was green. I hoped that somehow it would "detect" the contradictions in the assumptions.--

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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/904caba2-762e-49a2-bea5-1dc6a3506929n%40googlegroups.com.--

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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a244225f-f9a0-4db7-894c-cf52fd0bd762n%40googlegroups.com.

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+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5319e068-331e-4b62-9322-e9b695b98ec9n%40googlegroups.com.

**References**:**[tlaplus] Simple contradiction proof***From:*jack malkovick

**Re: [tlaplus] Simple contradiction proof***From:*Stephan Merz

**Re: [tlaplus] Simple contradiction proof***From:*jack malkovick

**Re: [tlaplus] Simple contradiction proof***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Simple contradiction proof** - Next by Date:
**[tlaplus] simple toy theorem** - Previous by thread:
**Re: [tlaplus] Simple contradiction proof** - Next by thread:
**[tlaplus] simple toy theorem** - Index(es):