This project is read-only.
Project Description
The TLA proof system is a prover for TLA written in Ocaml.

The TLA Proof System is an Ocaml prover for TLA. Since TLA is a first-order linear temporal logic, it proceeds mainly by processing a TLA formula into first-order classical logic and propositional temporal logic obligations.

Last edited Dec 9, 2013 at 9:14 PM by libal, version 2