Proof Tool Homepage

Proof Tool is a program to review sequent calculi proofs. It supports zooming and scrolling and some basic proof modification functions to make a proof better readable. Output and input format is XML to provide an easy interface to other applications.

News

2011/08/30: Prooftool beta 10 has been released, fixing bugs regarding compilation and relaxing rules for the xml parser.

Features

• LaTeX (proof.sty) like layout.
• Splitting proofs down into subproofs. By clicking on the name of a preceding or posterior proof you get there directly.
• Meta variables for complex formulas and sequences of formulas to reduce the length of sequents.
• Scheme scriptable by Guile.
• User interface is customizable.
• Export proofs for LaTeX and as PDF files.
• Import of otter's proof objects (type 2).
• Calculi independent.

Requirements

• Qt (version 3)
• Freetype 2
• Guile (at least version 1.6)
• libxml2 (at least version 2.6.7)
• PDFlib (Lite) (optional, at least version 5)

Download

Download beta 10 of Proof Tool here. In order to install Proof Tool correctly, follow the instructions in the INSTALL file which is contained in the src directory.

Documentation

Proof Tool is still under development, so documentation is very poor at this point.

• The XML DTD: proofdatabase.dtd

Links

• HLK is a compiler to generate LK proofs by defining them in a higher (LK) language.
• CERES is a tool for automated proof analysis. Input and output proofs can be displayed by the proof tool.

Contact

If you have any questions or encountered problems with Proof Tool, feel free to contact us: prooftool |@| logic |.| at