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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Thu, 24 Oct 2019 17:53:44 +0200*References*: <730a0c57-4a45-4205-817b-fa06a5852f0b@googlegroups.com>

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

**Follow-Ups**:

**References**:

- Prev by Date:
**[tlaplus] [TLAPS] Is there a way to see the steps taken by the automated prover to prove a goal ?** - Next by Date:
**Re: [tlaplus] [TLAPS] Is there a way to see the steps taken by the automated prover to prove a goal ?** - Previous by thread:
**[tlaplus] [TLAPS] Is there a way to see the steps taken by the automated prover to prove a goal ?** - Next by thread:
**Re: [tlaplus] [TLAPS] Is there a way to see the steps taken by the automated prover to prove a goal ?** - Index(es):