{"id":7649,"date":"2022-01-02T12:16:46","date_gmt":"2022-01-02T11:16:46","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7649"},"modified":"2022-01-02T12:16:46","modified_gmt":"2022-01-02T11:16:46","slug":"resena-computational-logic-its-origins-and-applications","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-computational-logic-its-origins-and-applications\/","title":{"rendered":"Rese\u00f1a: Computational logic: its origins and applications"},"content":{"rendered":"<p><a href=\"https:\/\/www.cl.cam.ac.uk\/~lp15\/\">Lawrence C. Paulson<\/a> public\u00f3 en 1998 el art\u00edculo <a href=\"https:\/\/royalsocietypublishing.org\/doi\/10.1098\/rspa.2017.0872\">Computational logic: its origins and applications<\/a> cuyo resumen es<\/p>\n<blockquote><p><a href=\"https:\/\/en.wikipedia.org\/wiki\/Computational_logic\">Computational logic<\/a> is the use of computers to establish facts in a logical formalism. Originating in nineteenth century attempts to understand the nature of mathematical reasoning, the subject now comprises a wide variety of formalisms, techniques and technologies. One strand of work follows the \u2018<a href=\"https:\/\/en.wikipedia.org\/wiki\/Logic_for_Computable_Functions\">logic for computable functions (LCF) approach<\/a>\u2019 pioneered by <a href=\"https:\/\/en.wikipedia.org\/wiki\/Robin_Milner\">Robin Milner<\/a>, where proofs can be constructed interactively or with the help of users\u2019 code (which does not compromise correctness). A refinement of LCF, called <a href=\"https:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle<\/a>, retains these advantages while providing flexibility in the choice of logical formalism and much stronger automation. The main application of these techniques has been to prove the correctness of hardware and software systems, but increasingly researchers have been applying them to mathematics itself.<\/p><\/blockquote>\n<p>y su contenido es<\/p>\n<ol class=\"org-ol\">\n<li>Introduction.<\/li>\n<li>A brief history of formal logic.<\/li>\n<li>Mechanized logic: the LCF tradition.<\/li>\n<li>A new theorem-proving architecture: Isabelle.<\/li>\n<li>Formalizing mathematics.<\/li>\n<li>Obstacles to formalizing mathematics.<\/li>\n<li>The way forward.<\/li>\n<\/ol>\n","protected":false},"excerpt":{"rendered":"<p>Lawrence C. Paulson public\u00f3 en 1998 el art\u00edculo Computational logic: its origins and applications cuyo resumen es Computational logic is the use of computers to establish facts in a logical formalism. Originating in nineteenth century attempts to understand the nature of mathematical reasoning, the subject now comprises a wide variety of formalisms, techniques and technologies&#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":[166,156,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\/7649"}],"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=7649"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7649\/revisions"}],"predecessor-version":[{"id":7650,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7649\/revisions\/7650"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7649"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7649"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7649"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}