Sentential Logic Truth Tree Solver

A new improved version of the Truth Tree Solver is now available at!

The Truth Tree Solver is a free-to-use web tool that determines the consistency of a set of logical sentences according to the rules of Sentential Logic (SL) (aka Propositional Logic or Propositional Calculus). Given a set of symbolic sentences, this tool constructs a truth tree and outputs its visual representation using the same format as in The Logic Book by Bergmann, Moor and Nelson.

You may indeed use this tool as an alternative to the Student Solutions, or even find the solution for problems of the book for which no solution has been provided.

STEP 1: Compose a sentence

Write a symbolic sentence in the text field below. You may add any letters with your keyboard and add special characters using the appropriate buttons. When your sentence is ready, click the "Add" button to add this sentence to your set. You may add additional sentences to your set by repeating this step.

Atomic Sentences:

STEP 2: Validate your set

STEP 3: Get the result

Finally you can generate a truth tree by clicking the "Generate the tree!" button below. If your can't see the button, it means your set of sentences is empty or that you already generated the tree.

Once the tree is generated, interpret the result. If all terminal nodes end with the cross-symbol (✕), then your set is inconsistent. On the other hand, if there is at least one terminal node without a cross-symbol, then your set is consistent.