🎓 Tutorial
Begin Your Proof
Enter the formula you wish to prove. The tree grows upward from this root.
— or generate a provable formula —
SYNTAX GUIDE
| /\ or \and | ∧ | conjunction |
| \/ or \or | ∨ | disjunction |
| -> or \to | → | implication |
| ~ or \neg | ¬ | negation |
| _|_ or \bot | ⊥ | falsum |
| ( ) | grouping | |
| \forall x. P or \all x. P | ∀ | universal |
| \exists x. P or \ex x. P | ∃ | existential |
| P(x,y) f(x) | predicates & functions | |
| Precedence (high→low): ¬ > ∧ > ∨ > → > ∀ ∃. All right-associative. Quantifier scope extends as far right as possible. | ||