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,StephanOn 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.