Logitext is an educational proof assistant for *first-order classical
logic* using the *sequent calculus*, in the same tradition as Jape, Pandora, Panda and Yoda.
It is intended to assist students who are learning *Gentzen trees*
as a way of structuring derivations of logical statements.
Underneath the hood, Logitext interfaces with Coq in order to check
the validity of your proof steps. The frontend is written in
Haskell and Ur/Web, and there is an
interesting story behind it which you can read about. Alternatively, get the source at
GitHub.

To get started, check out the tutorial, or dive right in and type in something to prove:

Here are some examples:

Logitext is case-sensitive: capitalized identifiers represent propositions and predicates, while lower-case identifiers represent functions and elements of the universe.

If you don't like classical logic, check out the intuitionistic version!