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

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 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/247BE5EB-9628-4E7A-958A-48DEB3004CEE%40gmail.com.