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

The pltl front-end

Given any TLA formula, this front-end rule compute a satisfiability equivalent propositional linear temporal formula. Please refer to the PLTL Front-end for more information.

Back-ends

Last edited Dec 5, 2013 at 1:02 PM by libal, version 4