Abstract
Wouldn’t it be nice to be able to conveniently use ordinary real number expressions within proof assistants? In this paper we outline how this can be done within a theorem proving framework. First, we formally establish upper and lower bounds for trigonometric and transcendental functions. Then, based on these bounds, we develop a rational interval arithmetic where real number calculations can be performed in an algebraic setting. This pragmatic approach has been implemented as a strategy in PVS. The strategy provides a safe way to perform explicit calculations over real numbers in formal proofs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abramovitz, M., Stegun, I.: Handbook of Mathematical Functions. National Bureau of Standards (1972)
Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol. 1281, pp. 515–530. Springer, Heidelberg (1997)
Ciaffaglione, A.: Certified Reasoning on Real Numbers and Objects in Coinductive Type Theory. PhD thesis, Università degli Studi di Udine (1993)
Daumas, M., Melquiond, G.: Generating formally certified bounds on values and round-off errors. In: Real Numbers and Computers, Dagstuhl, Germany, pp. 55–70 (2004)
Daumas, M., Melquiond, G., Muñoz, C.: Guaranteed proofs using interval arithmetic. In: Accepted for publication at the 17th IEEE Symposium on Computer Arithmetic (1995)
Dutertre, B.: Elements of mathematical analysis in PVS. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 141–156. Springer, Heidelberg (1996)
Fleuriot, J., Paulson, L.: Mechanizing nonstandard real analysis. LMS Journal of Computation and Mathematics 3, 140–190 (2000)
Gamboa, R.: Mechanically Verifying Real-Valued Algorithms in ACL2. PhD thesis, University of Texas at Austin (May 1999)
Gottliebsen, H.: Automated Theorem Proving for Mathematics: Real Analysis in PVS. PhD thesis, University of St Andrews (June 2001)
Gowland, P., Lester, D.: A survey of exact computer arithmetic. In: Blanck, J., Brattka, V., Hertling, P., Weihrauch, K. (eds.) Computability and Complexity in Analysis, CCA2000 Workshop, Swansea, Wales. Informatik Berichte, vol. 272, pp. 99–115. FernUniversität Hagen (2000)
Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK (1995)
Harrison, J.: Theorem Proving with the Real Numbers. Springer, Heidelberg (1998)
Hickey, T., Ju, Q., van Emden, M.H.: Interval arithmetic: from principles to implementation. Journal of the ACM (2001)
Kearfott, R.B.: Interval computations: Introduction, uses, and resources. Euromath Bulletin 2(1), 95–112 (1996)
Mayero, M.: Formalisation et automatisation de preuves en analyses réelle et numérique. PhD thesis, Université Paris VI, décembre (2001)
Ménissier, V.: Arithmétique Exacte : Conception, Algorithmique et Performances d’une Implantation Informatique en Précision Arbitraire. PhD thesis, Université Paris VI, Paris, France (1994)
Muñoz, C.: PVSio reference manual – Version 2.a (2004), Available from http://research.nianet.org/~munoz/PVSio
Muñoz, C., Carreño, V., Dowek, G., Butler, R.W.: Formal verification of conflict detection algorithms. International Journal on Software Tools for Technology Transfer 4(3), 371–380 (2003)
Niqui, M.: Formalising Exact Arithmetic: Representations, Algorithms and Proofs. PhD thesis, Radboud University Nijmegen (1994)
Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)
Pour-El, M., Richards, J.: Computability in Analysis and Physics. Perspectives in Mathematical Logic. Springer, Berlin (1989)
Robinson, R.M.: Review of Peter, R., Rekursive Funktionen. The Journal of Symbolic Logic 16, 280–282 (1951)
Shankar, N.: Efficiently executing PVS. Project report, Computer Science Laboratory, SRI International, Menlo Park (1999), Available at http://www.csl.sri.com/shankar/PVSeval.ps.gz
Specker, E.: Nicht konstruktiv beweisbare Sätze der Analysis. The Journal of Symbolic Logic 14(3), 145–158 (1949)
Turing, A.: On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society 42(2), 230–265 (1936)
von Henke, F.W., Pfab, S., Pfeifer, H., Rueß, H.: Case Studies in Meta-Level Theorem Proving. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 461–478. Springer, Heidelberg (1998)
Yakovlev, A.: Classification approach to programming of localizational (interval) computations. Interval Computations 1(3), 61–84 (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Muñoz, C., Lester, D. (2005). Real Number Calculations and Theorem Proving. In: Hurd, J., Melham, T. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2005. Lecture Notes in Computer Science, vol 3603. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11541868_13
Download citation
DOI: https://doi.org/10.1007/11541868_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28372-0
Online ISBN: 978-3-540-31820-0
eBook Packages: Computer ScienceComputer Science (R0)