CALCCHECK

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/.

Downloads

• 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:
  • MS Windows:
    • Zipped WindowsXP executable: CalcCheck-0.2.29_WindowsXP_exe.zip (1MB), contains just the file CalcCheck.exe (4.2MB)
    • If your MSWindows command prompt cannot handle Unicode, running CalcCheck may output some unreadable material. You can add the commandline flag -q and use the generated HTML file for feedback:

       >  CalcCheck -q MyProofs.ltx
      CalcCheck-0.2.24: No syntax errors.
      CalcCheck-0.2.24: Now checking...
      
      
      CalcCheck-0.2.24: Finished checking MyProofs.ltx
      CalcCheck-0.2.24: Wrote MyProofs.ltx.html
      

  • MacOS X:
    • Compiled on MacOS 10.6.8: CalcCheck-0.2.29_MacOS-X_executable.tar.gz (1.5MB) contains just the file CalcCheck (6.8MB)
  • Linux:
    • Gzipped 64bit Linux executable (statically linked): CalcCheck-0.2.29_linux_x86_64_static.gz

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

Publication

• Wolfram Kahl: The Teaching Tool CalcCheck: A Proof-Checker for Gries and Schneider's “Logical Approach to Discrete Math”, in J.-P. Jouannaud, Z. Shao (eds.): Certified Programs and Proofs, CPP 2011, pp. 216–230, LNCS 7086, Springer-Verlag, 2011.