{"id":3602,"date":"2013-09-10T08:24:16","date_gmt":"2013-09-10T06:24:16","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3602"},"modified":"2013-09-10T08:25:44","modified_gmt":"2013-09-10T06:25:44","slug":"from-tarski-to-hilbert","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/from-tarski-to-hilbert\/","title":{"rendered":"From Tarski to Hilbert"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento aproximado en <a href=\"http:\/\/coq.inria.fr\/\">Coq<\/a> sobre geometr\u00eda titulado <a href=\"http:\/\/hal.inria.fr\/docs\/00\/80\/36\/62\/PDF\/adg2012_braun_narboux_postproc.pdf\">From Tarski to Hilbert<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/gabrielbraun.free.fr\/\">Gabriel Braun<\/a> y <a href=\"http:\/\/dpt-info.u-strasbg.fr\/~narboux\/\">Julien Narboux<\/a> (de la Universidad de Estrasburgo, Francia).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nIn this paper, we report on the formal proof that Hilbert&#8217;s axiom system can be derived from Tarski&#8217;s system. For this purpose we mechanized the proofs of the first twelve chapters of Schwabauser, Szmielew and Tarski&#8217;s book: <a href=\"http:\/\/www.springer.com\/mathematics\/book\/978-3-642-69418-9\">Metamathematische Methoden in der Geometrie<\/a>. The proofs are checked formally within classical logic using the Coq proof assistant. The goal of this development is to provide clear foundations for other formalizations of geometry and implementations of decision procedures.\n<\/p><\/blockquote>\n<p>El trabajo se ha presentado en el <a href=\"http:\/\/dream.inf.ed.ac.uk\/events\/adg2012\/\">ADG 2012<\/a> (<i>Automated Deduction in Geometry 2012<\/i>) <\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Coq se encuentra <a href=\"http:\/\/dpt-info.u-strasbg.fr\/~narboux\/tarski.html\">aqu\u00ed<\/a> y <a href=\"http:\/\/gabrielbraun.free.fr\/Geometry\/Tarski\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento aproximado en Coq sobre geometr\u00eda titulado From Tarski to Hilbert. Sus autores son Gabriel Braun y Julien Narboux (de la Universidad de Estrasburgo, Francia). Su resumen es In this paper, we report on the formal proof that Hilbert&#8217;s axiom system can be derived from Tarski&#8217;s system. For this&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","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":[45,219,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\/3602"}],"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=3602"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3602\/revisions"}],"predecessor-version":[{"id":3604,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3602\/revisions\/3604"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3602"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3602"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3602"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}