Abstract
Assumptions about the domains of partial functions are necessary in state-of-the-art proof assistants. On the other hand when mathematicians write about partial functions they tend not to explicitly write the side conditions. We present an approach to formalizing partiality in real and complex analysis in total frameworks that allows keeping the side conditions hidden from the user as long as they can be computed and simplified automatically. This framework simplifies defining and operating on partial functions in formalized real analysis in HOL Light. Our framework allows simplifying expressions under partiality conditions in a proof assistant in a manner that resembles computer algebra systems.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abramowitz, M., Stegun, I.A.(eds.): Handbook of Mathematical Functions With Formulas, Graphs, and Mathematical Tables, United States Department of Commerce, Washington, D.C. National Bureau of Standards Applied Mathematics Series, vol. 55 (June 1964); 9th Printing, November 1970 with corrections
Aslaksen, H.: Multiple-valued complex functions and computer algebra. SIGSAM Bulletin (ACM Special Interest Group on Symbolic and Algebraic Manipulation) 30(2), 12–20 (1996)
Beeson, M.: Using nonstandard analysis to ensure the correctness of symbolic computations. Int. J. Found. Comput. Sci. 6(3), 299–338 (1995)
Bove, A., Capretta, V.: Modelling general recursion in type theory. Mathematical Structures in Computer Science 15(4), 671–708 (2005)
Coq Development Team. The Coq Proof Assistant Reference Manual Version 8.1. INRIA-Rocquencourt (2006)
Corless, R.M., Jeffrey, D.J.: Well ... it isn’t quite that simple. SIGSAM Bulletin (ACM Special Interest Group on Symbolic and Algebraic Manipulation) 26(3), 2–6 (1992)
Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN, the constructive Coq repository at Nijmegen. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 88–103. Springer, Heidelberg (2004)
Farmer, W.M., Guttman, J.D., Thayer, F.J.: imps: An Interactive Mathematical Proof System (system abstract). In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 653–654. Springer, Heidelberg (1990)
Farmer, W.M.: A scheme for defining partial higher-order functions by recursion. In: Butterfield, A., Haegele, K. (eds.) IWFM, Workshops in Computing. BCS (1999)
Harrison, J.: HOL light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265–269. Springer, Heidelberg (1996)
Kaliszyk, C., Wiedijk, F.: Certified computer algebra on top of an interactive theorem prover. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM/CALCULEMUS 2007. LNCS (LNAI), vol. 4573, pp. 94–105. Springer, Heidelberg (2007)
Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 589–603. Springer, Heidelberg (2006)
Lozier, D.W.: Nist digital library of mathematical functions. Ann. Math. Artif. Intell. 38(1-3), 105–119 (2003)
Müller, O., Slind, K.: Treating partiality in a logic of total functions. Comput. J. 40(10), 640–652 (1997)
Owre, S., Rushby, J., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)
Wiedijk, F., Zwanenburg, J.: First order logic with domain conditions. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 221–237. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kaliszyk, C. (2008). Automating Side Conditions in Formalized Partial Functions. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds) Intelligent Computer Mathematics. CICM 2008. Lecture Notes in Computer Science(), vol 5144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85110-3_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-85110-3_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85109-7
Online ISBN: 978-3-540-85110-3
eBook Packages: Computer ScienceComputer Science (R0)