CodePlexProject Hosting for Open Source Software

The TLA proof rules generates a TLA proof whose leaves are TLA formulas. Before these formulas can be sent to an external prover, the system determines (right now based only on the intended external prover) the proper unary front-end rule to apply.

More information about the TLA proof rules can be found in:

- Leslie Lamport's PerliminaryGuide.
- K. Chaudhuri, D. Doligez, L. Lamport and S. Merz, “A TLA+ Proof System”, Workshop on Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA). CEUR Workshop Proceedings 418, pp. 17–37. November 2008.

Last edited Dec 5, 2013 at 1:27 PM by libal, version 6