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

[Hengfeng Wei <hengxin0912@xxxxxxxxx>]

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,

hengxin

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