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.

References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Breitner, Joachim: Visual theorem proving with the Incredible Proof Machine (2016)