{"id":3227,"date":"2013-04-14T08:42:04","date_gmt":"2013-04-14T08:42:04","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3227"},"modified":"2013-04-14T08:42:04","modified_gmt":"2013-04-14T08:42:04","slug":"resena-one-logic-to-use-them-all","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-one-logic-to-use-them-all\/","title":{"rendered":"Rese\u00f1a: One logic to use them all"},"content":{"rendered":"<p>Una de las principales barreras en el avance de la automatizaci\u00f3n del razonamiento consiste en la comunicaci\u00f3n entre distintos sistemas de razonamiento. Una forma de superarla es la planteada en el art\u00edculo <a href=\"http:\/\/hal.inria.fr\/docs\/00\/80\/96\/51\/PDF\/main.pdf\">One logic to use them all<\/a>.<\/p>\n<p>Su autor es <a href=\"https:\/\/www.lri.fr\/~filliatr\">Jean-Christophe Filli\u00e2tre<\/a> (de la Universidad de Par\u00eds-Sur).<\/p>\n<p><p>El trabajo se presentar\u00e1 en el <a href=\"http:\/\/www.cade-24.info\">CADE-24<\/a> (24th International Conference on Automated Deduction). <\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n<a href=\"https:\/\/www.lri.fr\/perso\/~filliatr\/hdr\/memoire.pdf\">Deductive program verification<\/a> is making fast progress these days. One of the reasons is a tremendous improvement of theorem provers in the last two decades. This includes various kinds of automated theorem provers, such as ATP systems and SMT solvers, and interactive proof assistants. Yet most tools for program verification are built around a single theorem prover. Instead, we defend the idea that a collaborative use of several provers is a key to easier and faster verification. This paper introduces a logic that is designed to target a wide set of theorem provers. It is an extension of first-order logic with polymorphism, algebraic data types, recursive definitions, and inductive predicates. It is implemented in the tool <a href=\"http:\/\/why3.lri.fr\">Why3<\/a>, and has been successfully used in the verification of many non-trivial programs.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Una de las principales barreras en el avance de la automatizaci\u00f3n del razonamiento consiste en la comunicaci\u00f3n entre distintos sistemas de razonamiento. Una forma de superarla es la planteada en el art\u00edculo One logic to use them all. Su autor es Jean-Christophe Filli\u00e2tre (de la Universidad de Par\u00eds-Sur). El trabajo se presentar\u00e1 en el CADE-24&#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":[1],"tags":[285,207],"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\/3227"}],"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=3227"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3227\/revisions"}],"predecessor-version":[{"id":3229,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3227\/revisions\/3229"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3227"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3227"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3227"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}