Check for inference validity.

Uses a tableau procedure to check validity in formal logic (for now, either in truth-functional propositional logic or in the basic modal logics K and T.) If no premisses are given, it looks for a tautology.
Allowed symbols: lettersa-z and A-Z, except v., ¬ (or ~), ∧ (or &), ∨ (or v), → (or ⊃, ->), ↔ (or ≡, <->), (, ).
Done using Python and the forest package for LaTeX.