Interactive tools for a logic course. Each one takes a formula and works through a method step by step, checking every move rather than just handing over an answer.
They all read the same syntax:
¬ ∧ ∨ ⊃ ≡, with ⊃ for implication
and ≡ for the biconditional. Variables are letters.
The predicate page adds ∀ ∃, written
forall x and exists x. There the position decides
what a name is — p(…) is a predicate, f(…) inside
the brackets a function — and a quantifier reaches over one unit unless a
dot widens it. The modal page adds □ ◇, typed
[] and <>, which bind as tightly as
¬ does.
If those characters are awkward to type, ~ & | -> <-> work
just as well, as do !, /\, \/, =>
and the arrows → and ↔. Each page also has a row of
buttons that insert the symbols for you.