A TLA+ Proof System

Details A TLA+ Proof System A TLA+ Proof System

2008-11-12

arxiv.org/abs/0811.1914v1

Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA) (2008)

Computer Science

Logic in Computer Science

Scientific paper

We describe an extension to the TLA+ specification language with constructs for writing proofs and a proof environment, called the Proof Manager (PM), to checks those proofs. The language and the PM support the incremental development and checking of hierarchically structured proofs. The PM translates a proof into a set of independent proof obligations and calls upon a collection of back-end provers to verify them. Different provers can be used to verify different obligations. The currently supported back-ends are the tableau prover Zenon and Isabelle/TLA+, an axiomatisation of TLA+ in Isabelle/Pure. The proof obligations for a complete TLA+ proof can also be used to certify the theorem in Isabelle/TLA+.

Affiliated with

Also associated with

No associations

Rating

A TLA+ Proof System does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with A TLA+ Proof System, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A TLA+ Proof System will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-101232