GabLem.com

Predicate Logic Truth Tree Solver

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 either Sentential Logic (SL) (aka Propositional Logic or Propositional Calculus) or Predicate Logic (PL). 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.

If you are unfamiliar with Logic, or with the truth tree method for determining set consistency, you can try this application anyway by choosing the "Demo!" tab.

If you already know about truth trees and you are dying to find how to use this tool, you may now proceed by clicking on the formal system of your choice (Sentential Logic or Predicate Logic) and following the 3 easy steps.

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.

Predicates:
Terms:   
Connectives:
Quantifiers:
Parentheses:  

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.