πVC: The Pi Verifying
Compiler. This software accompanies COC.
Implementation of Cooper's
quantifier-elimination method for Presburger arithmetic (last updated
12/02/2007). The main code, for
those who want a quick look. See Chapter 7 of COC for an
explanation.