{"id":3150,"date":"2013-03-31T07:11:13","date_gmt":"2013-03-31T07:11:13","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3150"},"modified":"2013-03-31T07:19:43","modified_gmt":"2013-03-31T07:19:43","slug":"resena-formalization-of-the-complex-number-theory-in-hol4","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-formalization-of-the-complex-number-theory-in-hol4\/","title":{"rendered":"Rese\u00f1a: Formalization of the complex number theory in HOL4"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/hol.sourceforge.net\/\">HOL4<\/a> sobre n\u00fameros complejos titulado <a href=\"http:\/\/qpl.naturalspublishing.com\/files\/published\/j44lfykd8715l9.pdf\">Formalization of the complex number theory in HOL4<\/a>.<\/p>\n<p>Sus autores son Zhiping Shi, Liming Li, Yong Guan, Xiaoyu Song, Minhua Wu y Jie Zhang.<\/p>\n<p>Su resumen es <\/p>\n<blockquote><p>\nIn this paper, the theory of complex numbers is formalized and the theorem library of complex numbers is embedded in HOL4, the theorem prover of High Order Logics. The theorem library introduces a data type \u2102 by an \u211d \u00d7 \u211d type abbreviation, and defines arithmetic operations of complex numbers in terms of group and field theories. Moreover, the polar and exponential forms are provided for simplifying the applications in control theory and signal analysis. We define the scalar multiplication of complex numbers and prove some properties about \u211d-module of complex numbers. The theorem library extends the scope of application of HOL4. The developed complex number theory has been released in HOL4 Kananaskis-7.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en HOL4 sobre n\u00fameros complejos titulado Formalization of the complex number theory in HOL4. Sus autores son Zhiping Shi, Liming Li, Yong Guan, Xiaoyu Song, Minhua Wu y Jie Zhang. Su resumen es In this paper, the theory of complex numbers is formalized and the theorem library&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[199,273,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3150"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=3150"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3150\/revisions"}],"predecessor-version":[{"id":3153,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3150\/revisions\/3153"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3150"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3150"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3150"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}