The Structure of the Prover
The TLAPM (TLA Prover Module) proves TLA proofs by generating a TLA Proof whose leaves are proof obligations. Right now, the proof obligations can be either first-order formulas or propositional linear temporal formulas.
- Information about the TLA proof calculus can be found in the
TLA Proof Calculus documentation.
The Front-end Proof Rules
Right now they are being applied automatically to TLA formulas according to the chosen back-ends.
The action front-end
Given a TLA formula without temporal operators but with possibly actions, this front-end rule compute a satisfiability equivalent first-order formula by the use of
The pltl front-end
Given any TLA formula, this front-end rule compute a satisfiability equivalent propositional linear temporal formula. Please refer to the
for more information.