CVC: a Cooperating Validity Checker

Note: CVC is no longer supported.
It is replaced by CVC Lite.
In particular, known bugs will no longer be fixed

CVC is a program for checking logical validity of certain kinds of formulas. The formulas can contain propositional operators like AND, OR, NOT, and => ("implies"). They can also contain equations between certain mathematical terms, and atomic formulas like "x < y". An example is

(f(x + y) = 3*y/2 AND x = y/2) => (f(f(x + y)) = 3*x)

This formula is logically valid, in the sense that any assignment of numbers to x and y will make the formula true, no matter what the function f is.