| Hello, the default strategy of TLAPS is to try first the SMT backend, then Zenon, then Isabelle (with the "auto" tactic). As long as your proof obligation is proved, you don't need to worry which backend succeeded. You can find out by looking at the proof console and then document this by adding "BY Zenon" etc. so that you don't have to wait for the other backends to timeout. Generally, SMT helps with obligations involving arithmetic and basic reasoning about sets and functions. Its main weakness is reasoning about formulas with quantifiers (explicitly present in the proof obligation or generated from the encoding of set theory). Zenon is usually more successful for obligations involving first-order logic (quantifiers) and set theory, but it doesn't know anything about arithmetic. Isabelle occasionally proves one-off goals that SMT or Zenon don't catch but is mainly useful for goals involving schematic variables (technically, second-order unification) such as induction proofs. Isabelle contains other proof methods than "auto" that can be invoked as IsaM("blast") or IsaM("force") but knowledge about the inner workings of the backend is necessary to be able to use them effectively. Reasoning about sequences, finite sets and cardinality, bags, and recursive function definitions is currently not (or hardly) supported by the automated backends. You need to explicitly invoke theorems from library modules (including SequenceTheorems.tla, FiniteSetTheorems.tla, NaturalsInduction.tla, WellFoundedInduction.tla). You may want to look at the versions of these modules with proofs to get a feel for how to conduct proofs about these structures. Suggestions for useful lemmas that should be included in the library are always welcome. And we should certainly produce a tutorial for using TLAPS ... Hope this helps, 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/637DCE0D-4C72-497A-A340-4AE96D23BF27%40gmail.com. |