Willow is a web-based application for creating and validating truth trees. Truth trees build upon the short truth table method. They work in the same way except when there are no forced truth assignments, the tree branches into two sub-trees. You may read more about truth trees here.
- Option 1: Open Willow in a new tab https://willow.bram-hub.com
- Option 2: Click
File>New
- Option 1: Click
File>Savethis will save the truth tree with the existing file name. - Option 2: Click
File>Save as...this will allow you to choose file name before saving.
- Click
File>Openbrowse until you find the.willowfile you wish to open. Note that this will clear your current tree
Willow tries to be flexible with syntax but there are a few rules you must follow for Willow to correctly parse your truth tree.
Everyone has their own preferred logical symbols. Willow is smart and allows you to use a number of different options. You may use or even mix and match any of the following options.
| Symbol | Options |
|---|---|
| Negation | not ¬ ! ~ |
| Disjunction | or ∨ | |
| Conjunction | and ∧ & |
| Implication | implies only if → $ -> |
| Equivalence | iff equiv ↔ % <-> |
| Universal Quantifier | forall ∀ |
| Existential Quantifier | exists ∃ |
| Open Branch | ◯ |
| Closed Branch | × |
Also note that variables and function symbols must be lowercase. For example forall x is valid but forall X is invalid.
Predicates and propositions must be capitalized.
For example, writing A is valid, however a is invalid.
In addition, writing P(x) is valid, however p(x) is invalid.
¬((A ∨ B) ∧ (C → D)) ↔ E
~((A | B) & (C $ D)) % E
not ((A or B) and (C implies D)) iff E
¬((A | B) and (C -> D)) equiv E
∀x ∃y (P(x) ∧ Q(y))
Statements are First-order logic expressions in textboxes. To the left of each statement is a symbol representing one of three possibilities. A green check mark signifies your statement is a logical consequence and is correctly decomposed within the tree. A red "X" signifies an issue with that statement; hovering your mouse over this "X" will give you more information regarding the issue. A yellow triangle signifies that the statement itself is not recognized by the First-order logic expression parser*. In addition to these symbols, the currently selected statement is highlighted blue, its decomposition is highlighted red, and its logical "parent" is highlighted green.
*If you believe you wrote a valid FOL statement but it is not recognized, please contact a developer.
To add a node, click on a valid statement in the truth tree. To add a new statement below the currently selected statement click Edit>Add statement after or press ctrl+a(default). To add one above click Edit>Add statement before or press ctrl+b(default).
To split the truth tree into two branches, click on a statement. Then click Edit>Create branch or press ctrl+shift+b(default).
To remove a statement, click on a statement. Then click Edit>Delete statement or press ctrl+d(default).
To remove a branch, click on any statement within a branch. Then click Edit>Delete branch or press ctrl+shift+d(default).
To add a premise, click on a valid statement in the truth tree and then click Edit>Toggle premise or press ctrl+p(default)
A premise is denoted by the word Premise to the right of the input text box
A correctly decomposed premise will be indicated by a green checkmark to the left of the input text box
- To decompose a premise/statement first add the correct branches/statements that it decomposes into. You can read more about valid decomposition rules here
- You now have 2 options
a) If you would like to decompose the current statement, right click all the statements below it in the tree that it decomposes into. These statements will turn red and will say decomposes into.
b) If you would like to select the statements that the current statements are the logical consequence of, right click all the statements above it in the tree that it was decomposed from. These statements will turn green and will say logical consequence of.
Assuming you did it correctly, your statement should now have a green check mark to the right of the input text box.
A truth tree is only complete when it has been fully decomposed. There are 2 ways to fully decompose a truth tree. A truth tree that has any branch that terminates with an open statement (◯) is fully decomposed. Otherwise a truth tree will be fully decomposed when all branches terminate with a closed statement (×).
You may check the truth tree is valid by clicking Evaluate>Check correctness
As your truth tree grows, it may make it hard to follow what is going on. Willow allows you to collapse branches to hide them from the screen. Do not worry, a collapsed branch will still be used when Willow is evaluating your tree, these branches are just hidden from the user.
- Hiding a branch: Click the downward facing chevron next to the first statement in any branch.
- Unhiding a branch: Click the rightward facing chevron next to the first statement in a hidden branch
Willow has a number of keyboard shortcuts to help you when making a truth tree. You can modify any of the shotcuts by clicking Options>Shortcuts
The default list of shortcuts are as follows:
| Symbol | Options |
|---|---|
| Toggle premise | ctrl+p |
| Add statement before | ctrl+b |
| Add statement after | ctrl+a |
| Create branch | ctrl+shift+b |
| Delete statement | ctrl+d |
| Delete branch | ctrl+shift+d |
Willow has 2 themes, a dark mode and a light mode. To toggle betweent the two themes, click Options>Toggle Theme
