# 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:

• Processes proofs contained in LaTeX documents:
Invocation, in a terminal (respectively command prompt):
  CalcCheck MyProofs.ltx

• Checks individual steps of calculational proofs
• Checks whether a calculation proves its goal

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

The homepage of CalcCheck is http://CalcCheck.McMaster.ca/.

• CalcCheckManual.pdf (updated 2013-01-13): A brief introduction to writing math for CalcCheck.
• The LaTeX package CalcStyleV9.sty is required for typesetting the math understood by the current version of CalcCheck. (This requires a TeX installation with a large amount of mathematics-related macro packages; these can be found for example in the Ubuntu package texlive-math-extra.)
• Source distribution: CalcCheck-0.2.29.tar.gz or CalcCheck-0.2.29.zip

• Unpack: tar xzf CalcCheck-0.2.29.tar.gz
• Go into the unpacked directory: cd CalcCheck-0.2.29
• Least potential for complications:
  ghc --make Setup
./Setup configure
./Setup build
./Setup install

will install CalcCheck most likely into /usr/local/bin, which should be in your default PATH anyway.

(On most UNIX-like systems, including MacOS X, you probably need to execute the last step prefixed with “sudo”.)

• Alternatively, if you have cabal-install (included in the Haskell platform) and have used it before:

Simply say: cabal install

This should produce an executable, and install it (at least on UNIX-like systems) into .cabal/bin in your home directory. If you have that directory in your PATH, it should be found no matter from which directory you issue CalcCheck commands.

• Precompiled executables:

## Example

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 \end{calc} 

LaTeX result:

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