Animated truth-functional evaluation of a well-formed formula via a parse tree. The visualization cycles through all truth assignments for atomic propositions p and q, computes each subformula bottom-up (including ¬ and ->), and highlights the corresponding truth-table row to illustrate satisfiability (exists a true row) and validity (all rows true).
Pure Canvas2D, green-on-black blocky UI with grid snapping. Cycles through 4 assignments (p,q) on a fixed WFF (p->q)->(¬p->q). Uses staged easing within each step to animate bottom-up semantics and row highlighting; computes satisfiable/valid from the full truth table each frame.