Propositional symbols must begin with a letter, and can be followed by letters or numbers. For example, "Rainy", "Car1", etc.
The following operators are recognized:
Parentheses may be used to group sub-propositions, but make sure they are balanced.
Operator precedence is shown in the list of operators, with higher-precedence operators appearing higher in the list.
Parentheses take precedence over all operators.
If you're unsure if your syntax is correct, verify the parsed expression below.
Results are displayed in a tree, with each node representing a sequent. A sequent is an axiom if its assumptions and conclusions share a common proposition. A node is finished if it is an axiom, or if its assumptions and conclusions consist of only atomic symbols.
All unfinished nodes are expanded, that is to say, inference rules are applied to them to manipulate the propositions between the assumptions and conclusions.
When all nodes in the tree are finished, the deduction tree is complete, and is displayed graphically below. Axioms are highlighted in green. Finished non-axioms are highlighted in red.
If, once the tree is finished, all leaves of the tree are axioms, then the original proposition is a tautology (i.e. it is always true). If any leaves are not axioms, the original proposition is not a tautology, and any non-axiom leaves contain the counter-examples to disprove it.
TLDR: If all your tree's leaves are green, the proposition is true. If any leaves are red, it is false, and the red leaves are the counterexamples.
For more information, check the Gentzen wiki.