{"id":4960,"date":"2015-08-12T07:35:59","date_gmt":"2015-08-12T05:35:59","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4960"},"modified":"2015-08-12T07:35:59","modified_gmt":"2015-08-12T05:35:59","slug":"resena-a-synthetic-proof-of-pappus-theorem-in-tarskis-geometry","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-a-synthetic-proof-of-pappus-theorem-in-tarskis-geometry\/","title":{"rendered":"Rese\u00f1a: A synthetic proof of Pappus\u2019 theorem in Tarski\u2019s geometry"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/coq.inria.fr\/\">Coq<\/a> sobre geometr\u00eda titulado <a href=\"https:\/\/hal.inria.fr\/hal-01176508\/document\">A synthetic proof of Pappus\u2019 theorem in Tarski\u2019s geometry<\/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> (del <a href=\"http:\/\/bit.ly\/1hsWEmk\">\u00c9quipe Informatique G\u00e9om\u00e9trique et Graphique<\/a> en la Universidad de Estrasburgo, Francia).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  In this paper, we report on the formalization of a synthetic proof of Pappus&#8217; theorem. We provide two versions of the theorem: the first one is proved in neutral geometry (without assuming the parallel postulate), the second (usual) version is proved in Euclidean geometry. The proof that we formalize is the one presented by Hilbert in <a href=\"https:\/\/www.gutenberg.org\/files\/17384\/17384-pdf.pdf\">The Foundations of Geometry<\/a> which has been detailed by Schwabh\u00e4user, Szmielew and Tarski in part I of <a href=\"http:\/\/bit.ly\/1N7hYd2\">Metamathematische Methoden in der Geometrie<\/a>. We highlight the steps which are still missing in this later version. The proofs are checked formally using the Coq proof assistant. Our proofs are based on Tarski&#8217;s axiom system for geometry without any continuity axiom. This theorem is an important milestone toward obtaining the arithmetization of geometry which will allow us to provide a connection between analytic and synthetic geometry.\n<\/p><\/blockquote>\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>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre geometr\u00eda titulado A synthetic proof of Pappus\u2019 theorem in Tarski\u2019s geometry Sus autores son Gabriel Braun y Julien Narboux (del \u00c9quipe Informatique G\u00e9om\u00e9trique et Graphique en la Universidad de Estrasburgo, Francia). Su resumen es In this paper, we report on the formalization of a&#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,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\/4960"}],"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=4960"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4960\/revisions"}],"predecessor-version":[{"id":4961,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4960\/revisions\/4961"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4960"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4960"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4960"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}