ProofTools For Linux

ProofTools is a freely distributed and multiplatform software project that has been designed from the offset to be used for automatic and graphical generation of semantic tableaux, also known as semantic trees, analytic tableaux, proof trees or truth trees.

The application can be used to test whether an argument or proof is deductively valid, or whether a formula is a logical truth. ProofTools is capable of drawing proof trees for predicate, including identity, propositional and basic, normal, contingent-identity or constant domain modal logics. The program can export the final result to an image.

ProofTools’ graphical user interface boasts a simple design, it is easy to use and straightforward, and compresses all of its tools into a single window, so users can quickly access them and create proof of trees.

It allows users to change the interface’s or tree’s font, change the background and foreground color of the tree, set hotkeys, select modal logic variants, add premise, set conclusion, enable smooth lines, Tarski’s world syntax, abbreviate tree, and many other useful functions.

ProofTools is an application that uses both GTK+ and Qt cross-platform GUI toolkits for its graphical user interface. It has been written entirely in the Lazarus visual integrated development environment (IDE) and supports GNU/Linux, Microsoft Windows and Mac OS X operating systems.

The software is available for download for free, as pre-built binary packages with either the GTK+ or Qt GUIs, designed to support both 32-bit (x86) and 64-bit (x86_64) instruction set architectures. Please note that this is not an open-source application, so you won’t be able to download its source code.