{"id":5465,"date":"2016-07-29T07:35:36","date_gmt":"2016-07-29T05:35:36","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5465"},"modified":"2016-07-29T07:35:36","modified_gmt":"2016-07-29T05:35:36","slug":"resena-verification-of-an-lcf-style-first-order-prover-with-equality","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-verification-of-an-lcf-style-first-order-prover-with-equality\/","title":{"rendered":"Rese\u00f1a: Verification of an LCF-style first-order prover with equality"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre metal\u00f3gica titulado <a href=\"http:\/\/www.in.tum.de\/~nipkow\/Isabelle2016\/Isabelle2016_10.pdf\">Verification of an LCF-style first-order prover with equality<\/a>.<\/p>\n<p>Sus autores son Alexander Birch Jensen, <a href=\"https:\/\/people.compute.dtu.dk\/andschl\">Anders Schlichtkrull<\/a> y <a href=\"http:\/\/www2.compute.dtu.dk\/~jovi\">J\u00f8rgen Villadsen<\/a> (del grupo <a href=\"http:\/\/www.compute.dtu.dk\/english\/research\/Algolog\">Algorithms, logic and graphs<\/a> en la <em>Technical University of Denmark (DTU)<\/em>)<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  We formalize in Isabelle\/HOL the kernel of an LCF-style prover for first-order logic with equality from John Harrison\u2019s <em>Handbook of Practical Logic and Automated Reasoning<\/em>. We prove the kernel sound and generate Standard ML code from the formalization. The generated code can then serve as a verified kernel. By doing this we also obtain verified components such as derived rules, a tableau prover, tactics, and a small declarative interactive theorem prover. We test that the kernel and the components give the same results as Harrison\u2019s original on all the examples from his book. The formalization is 600 lines and is available online.\n<\/p><\/blockquote>\n<p>El trabajo se presentar\u00e1 en el <a href=\"http:\/\/www21.in.tum.de\/~nipkow\/Isabelle2016\">Isabelle Workshop 2016<\/a>.<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en se encuentra <a href=\"https:\/\/github.com\/logic-tools\/sml-handbook\">aqu\u00ed<\/a>.<\/p>\n<p>Este art\u00edculo puede servir de lectura complementaria en los cursos de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra\">Razonamiento autom\u00e1tico<\/a>, <a href=\"http:\/\/www.cs.us.es\/cursos\/rac\/\">Razonamiento asistido por ordenador<\/a> y <a href=\"http:\/\/www.cs.us.es\/~mjoseh\/LCyTM-15\">L\u00f3gica computacional y teor\u00eda de modelos<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre metal\u00f3gica titulado Verification of an LCF-style first-order prover with equality. Sus autores son Alexander Birch Jensen, Anders Schlichtkrull y J\u00f8rgen Villadsen (del grupo Algorithms, logic and graphs en la Technical University of Denmark (DTU)) Su resumen es We formalize in Isabelle\/HOL the kernel of&#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":[144,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\/5465"}],"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=5465"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5465\/revisions"}],"predecessor-version":[{"id":5466,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5465\/revisions\/5466"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5465"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5465"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5465"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}