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

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.

On Thu, Oct 24, 2019 at 11:53 AM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:

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

On 24 Oct 2019, at 17:39, Saswata Paul <paulsaswata1@xxxxxxxxx> wrote:

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

--
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/730a0c57-4a45-4205-817b-fa06a5852f0b%40googlegroups.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/247BE5EB-9628-4E7A-958A-48DEB3004CEE%40gmail.com.