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

[tlaplus] Any instructions on when and how to explicitly specify backend provers in TLAPS proofs?

Dear All,

I am learning TLAPS proofs by following the "official" examples released with TLAPS.

I notice that sometimes we need to explicitly specify the backend provers,
like "BY IsaM("force")", "BY Z3", "BY SMT", and so on.

But, I have no idea which one/ones to choose (and in which situations).

What are the strengths/weaknesses of these backend provers?
Are there any instructions on when and how to explicitly specify some (which?) backend provers?

Best regards,

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/e90c0e0f-206a-4f9f-aa60-fb9899240aba%40googlegroups.com.