TEST YOUR METTLE!
                        -----------------

These test problems were developed to test the efficacy of new PVS
strategies and auto-rewrite libraries designed to support reasoning
about formulas involving real numbers.

These test problems are provided in the PVS syntax, but could easily
be translated into the syntax of other theorem provers.  (One day I
would like to create an html or latex version of these problems.)  It
would be interesting to see how other theorem provers handle these
formulas.

The current proofs of these problems rely on the Di Vito strategies
available on this web page.