TLA Proof Calculus

The calculus consists of TLA proof rules and front-end proof rules.

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:

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