Formulas should be written in LISP notation with parentheses. The following operators are supported:
| Operator |
Symbols |
Example |
| AND |
and, &, &&, ∧ |
(and P Q) |
| OR |
or, |, ||, ∨ |
(or P Q) |
| NOT |
not, !, ¬, ~ |
(not P) |
| IMPLIES |
implies, ->, =>, ⇒, → |
(implies P Q) |
| IFF |
iff, <=>, <->, ≡, ⇔ |
(iff P Q) |
About the Method
The method of analytical tableaux systematically searches for models of a logical formula by trying to construct a model where the formula is false. If all branches close (contain contradictions), the formula is a tautology.
- Open branches that can be expanded
- Closed branches (contradictions)
- Branches that can't progress
Keyboard Shortcuts
P Parse formula
R Run full proof
N Next step
B Step back
C Clear