# 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