[TLAPS] Is there a way to see the steps taken by the automated prover to prove a goal ?

[Saswata Paul]

Hi,

   Is there a way to see the steps taken by the automatic backend provers in order to prove a goal ("path to success") and to know exactly which lemmas/assumptions were used?

Thank you

[Stephan Merz]

Hi,

currently we do not export detailed proofs from the automatic backends. What would be your use case for such detailed proofs? Most of the backends could export a proof trace, and we imagine that such traces could be useful for certifying the proof by a trusted backend such as Isabelle/TLA+. (There is an option to do this for proofs found by Zenon.) However, proof obligations often undergo quite significant transformations between the TLA+ statement and  the formulas that are sent to the backend, so I am skeptical that a proof trace would be intelligible at the TLA+ level.

It would probably not be so difficult to extract the user-provided facts that were actually used in a proof, although the transformations done in pre-processing would again have to be tracked.

Regards,

Stephan

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/730a0c57-4a45-4205-817b-fa06a5852f0b%40googlegroups.com.

[Saswata Paul]

   A proof trace would allow us to detect if asserted assumptions which are wrong are being used by the backend provers to prove a goal.

   For example, for the proof of Paxos,  if we wrongly assert that ~ ({} SUBSET Quorums) <which should be equivalent to FALSE since SUBSET gives the powerset> instead of using \A Q \in Quorums : Q # {}, the backend provers may use this FALSE to prove any goal. 

   Therefore, if we can see the trace to make sure that a wrong assumption like FALSE has not been used by the backend, it will allow us to trust the proofs better. Sometimes, wrong assumptions which are not very evident may escape our notice while writing the specification.

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/yTQfEdEdQzQ/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/247BE5EB-9628-4E7A-958A-48DEB3004CEE%40gmail.com.

[Stephan Merz]

So what you are saying is that when you find out that some assumption that you asserted was actually wrong, you'd like to know where it was used in the proof.

We advise users to thoroughly model check their specifications before embarking on any proof. In our experience, using the model checker is a great way for validating a spec. (It could certainly detect the fallacy in the example that you give.) Doing so helps you avoid the problem in the first place.

Second, the proof system has an approximation for the functionality that you request: when you modify the assertion of some fact (or change a definition), you can relaunch the prover. Since all previous results of proof attempts are cached, steps that do not syntactically depend on the definition or fact will not be rechecked, and you quickly see which steps fail. Of course, if your assumption appears in a global USE, all steps will need to be reproved.

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAHeFUE8DXzp0yb53G85bHBkVa1EvkogePYhC%3DnpTdRa6Grz5TA%40mail.gmail.com.

[Saswata Paul]

Thank you for your reply.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/85FC19AF-DD4C-479F-B36B-1DF1F3D53F47%40gmail.com.