ProofTools iconProofTools 0.4.1 Beta

This project provides a free and cross-platform application for generating proof trees
ProofTools is a free graphical application written in both GTK+ and Qt, and designed to be used for automatic and graphical generation of semantic tableaux, also known as proof trees, analytic tableaux, or semantic 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 able to validate a propositional, a predicate and a modal logic argument or logical truth using the proof tree method.

ProofTools is a platform-independent application that supports Linux, Microsoft Windows and Mac OS X operating systems. Binaries for GTK and Qt are provided in the download section above, supporting both 32-bit and 64-bit architectures.

last updated on:
November 7th, 2013, 22:52 GMT
developed by:
Laird Shaw
license type:
ROOT \ Education


In a hurry? Add it to your Download Basket!

user rating



1 Screenshot
ProofTools - The main window, where users can generate proof trees
What's New in This Release:
  • Bugfix: the Substitutivity of Identicals rule was not being applied to identities themselves, such that the logical truth (a=b∧c=b)→a=c was not being evaluated as a logical truth.
  • Bugfix: world numbers were sometimes displaying when they shouldn't have.
  • Bugfix: the form was oversize on initial opening on OS X.
  • Changed a symbol replacement: \/ (backslash, forward slash) is now replaced with the disjunction operator, ∨, rather than the universal quantifier, ∀.
read full changelog

Add your review!