A Formal Proof of Cauchy’s Residue Theorem

详细信息    查看全文

• 刊名：Lecture Notes in Computer Science
• 出版年：2016
• 出版时间：2016
• 年：2016
• 卷：9807
• 期：1
• 页码：235-251
• 全文大小：309 KB
• 参考文献：1.Ahlfors, L.V.: Complex Analysis: An Introduction to the Theory of Analytic Funtions of One Complex Variable. McGraw-Hill, New York (1966)
  2.Avigad, J., Hölzl, J., Serafin, L.: A formally verified proof of the central limit theorem. CoRR abs/1405.7012 (2014)
  3.Bak, J., Newman, D.: Complex Analysis. Springer, New York (2010)CrossRef MATH
  4.Basu, S., Pollack, R., Roy, M.F.: Algorithms in Real Algebraic Geometry, vol. 10. Springer, Heidelberg (2006)MATH
  5.Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41–62 (2014)MathSciNet CrossRef MATH
  6.Brunel, A.: Non-constructive complex analysis in Coq. In: 18th International Workshop on Types for Proofs and Programs, TYPES 2011, Bergen, Norway, pp. 1–15, 8–11 September 2011
  7.Bruno Brosowski, F.D.: An elementary proof of the Stone-Weierstrass theorem. Proc. Am. Math. Soc. 81(1), 89–92 (1981)MathSciNet CrossRef MATH
  8.Caviness, B., Johnson, J.: Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, New York (2012)
  9.Conway, J.B.: Functions of One Complex Variable, vol. 11, 2nd edn. Springer, New York (1978)CrossRef
  10.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)CrossRef
  11.Hales, T.C., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, T.L., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., Nguyen, T.Q., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, A.H.T., Tran, T.N., Trieu, D.T., Urban, J., Vu, K.K., Zumkeller, R.: A formal proof of the Kepler conjecture. arXiv:​1501.​02155 (2015)
  12.Harrison, J.: Formalizing basic complex analysis. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, vol. 10(23), pp. 151–165. University of Białystok (2007)
  13.Harrison, J.: Formalizing an analytic proof of the Prime Number Theorem (dedicated to Mike Gordon on the occasion of his 60th birthday). J. Autom. Reasoning 43, 243–261 (2009)CrossRef
  14.Harrison, J.: The HOL light theory of Euclidean space. J. Autom. Reasoning 50, 173–190 (2013)MathSciNet CrossRef MATH
  15.Lang, S.: Complex Analysis. Springer, New York (1993)CrossRef MATH
  16.Stein, E.M., Shakarchi, R.: Complex Analysis, vol. 2. Princeton University Press, Princeton (2010)MATH
  
• 作者单位：Wenda Li (15)
  Lawrence C. Paulson (15)
  
  15. Computer Laboratory, University of Cambridge, Cambridge, UK
  
• 丛书名：Interactive Theorem Proving
• ISBN：978-3-319-43144-4
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349
• 卷排序：9807

文摘

We present a formalization of Cauchy’s residue theorem and two of its corollaries: the argument principle and Rouché’s theorem. These results have applications to verify algorithms in computer algebra and demonstrate Isabelle/HOL’s complex analysis library.