A Proof-Checker for Gries and Schneider’s
“Logical Approach to Discrete Math”

CalcCheck is a proof checker for calculational proofs in the logics of the popular textbook A Logical Approach to Discrete Math (LADM) by David Gries and Fred Schneider.

Main features:

CalcCheck is implemented in Haskell and is still under development. Bug reports and suggestions for improvements are very welcome.

The homepage of CalcCheck is



LaTeX input:

\begin{calc}[(3.16) $(p \nequiv q) \equiv (q \nequiv p)$]
    p \nequiv q
  \CalcStep{=}{Def.~of $\nequiv$ (3.10)}
    \lnot(p \equiv q)
  \CalcStep{=}{Symmetry of $\equiv$ (3.2)}
    \lnot(q \equiv p)
  \CalcStep{=}{Def.~of $\nequiv$ (3.10), with $p, q \becomes q, p$}
    q \nequiv p

LaTeX result:

<LaTeX output>

CalcCheck HTML output:

Proving  (3.16)  (p ≢ q) ≡ (q ≢ p):

    p ≢ q
  =   ⟨ Def.~of $\nequiv$ (3.10) ⟩
       — CalcCheck-0.2.12: (3.10) Definition of ≢   ─   OK

    ¬(p ≡ q)
  =   ⟨ Symmetry of $\equiv$ (3.2) ⟩
       — CalcCheck-0.2.12: (3.2) Symmetry of ≡   ─   OK (no change)

    ¬(q ≡ p)
  =   ⟨ Def.~of $\nequiv$ (3.10), with $p, q \becomes q, p$ ⟩
       — CalcCheck-0.2.12: (3.10) Definition of ≢   ─   OK

    q ≢ p

 — CalcCheck-0.2.12: Proof matches goal ─ OK


Wolfram Kahl