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:

• ((A -> B) -> A) -> A
• A \/ ~A
• (forall x, P(x)) -> (exists x, P(x))

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!