References

1

W. W. Bledsoe. A new method for proving certain Presburger formulas. Fourth Intl. Joint Conf. on A.I., Tblisi, USSR, September 1975.

2

Robert L. Constable, S. Johnson, and C. Eichenlaub. Introduction to the PL/CV2 Programming Logic, Lecture Notes in Computer Science, Vol. 135. Springer-Verlag, NY, 1982.

3

Max B. Forester. Formalizing constructive real analysis. Technical Report TR93-1382, Computer Science Dept., Cornell University, Ithaca, NY, 1993.

4

Paul B. Jackson. The Nuprl Proof Development System, Version 4.1 Reference Manual and User's Guide. Cornell University, Ithaca, NY, February 1994.

5

R.E. Shostak. A practical decision procedure for arithmetic with function symbols. J. Assoc. Comput. Mach., 26:351--360, 1979.

6

Todd Wilson. A formalization of the supinf algorithm. To appear 1996.