{"id":30198,"date":"2013-11-04T02:35:08","date_gmt":"2013-11-04T06:35:08","guid":{"rendered":"http:\/\/sosuaonline.net\/inicio\/qverificacion-informatica-de-la-existencia-de-diosq-y-filosofia-asistida-por-ordenadores\/"},"modified":"2013-11-04T02:35:08","modified_gmt":"2013-11-04T06:35:08","slug":"qverificacion-informatica-de-la-existencia-de-diosq-y-filosofia-asistida-por-ordenadores","status":"publish","type":"post","link":"https:\/\/sosuaonline.net\/inicio\/qverificacion-informatica-de-la-existencia-de-diosq-y-filosofia-asistida-por-ordenadores\/","title":{"rendered":"\u00abVerificaci\u00f3n inform\u00e1tica de la existencia de Dios\u00bb\u2026 y filosof\u00eda asistida por ordenadores"},"content":{"rendered":"

\"dios_segun_las_computadoras\"Cient\u00edficos demuestran con dos port\u00e1tiles la utilidad del razonamiento automatizado, tanto para la especulaci\u00f3n humana como para la inteligencia artificial. <\/p>\n

\u201cInvestigadores prueban la existencia de Dios con un programa de ordenador\u201d, han publicado numerosos medios. En realidad, lo que han conseguido los investigadores Christoph Benzm\u00fcller y Bruno Woltzenlogel ha sido validar inform\u00e1ticamente un teorema del matem\u00e1tico austr\u00edaco Kurt G\u00f6del que se\u00f1alaba que, desde el punto de vista de la l\u00f3gica, el argumento de la existencia de Dios es v\u00e1lido. Los cient\u00edficos nos detallan en la siguiente entrevista las implicaciones de este logro. Por Yaiza Mart\u00ednez. <\/p>\n

\n
\n
\"Kurt<\/a> <\/p>\n
<\/div>\n<\/p><\/div>\n
\n
\n
\n
\n
\u201cInvestigadores prueban la existencia de Dios con un programa de ordenador\u201d, han publicado en las \u00faltimas semanas diversos medios, como el alem\u00e1n <\/span>Die Welt<\/a>. <\/span><\/div>\n<\/p><\/div>\n<\/p><\/div>\n<\/p><\/div>\n<\/p><\/div>\n
\n

En realidad, lo que han conseguido los investigadoresChristoph Benzm\u00fcller<\/a>, de la Universidad Libre de Berl\u00edn en Alemania, y Bruno Woltzenlogel Paleo <\/a>de la Universidad T\u00e9cnica de Viena<\/a> en Austria, es validar inform\u00e1ticamente un teorema<\/a>del renombrado matem\u00e1tico austr\u00edaco Kurt G\u00f6del<\/a> que se\u00f1alaba que, desde el punto de vista de la l\u00f3gica, el argumento de la existencia de Dios es v\u00e1lido. <\/p>\n

Como explicaba a SINC<\/a> recientemente el matem\u00e1tico Jorge L\u00f3pez Abad, del ICMAT: \u201cLo que han hecho estos autores es formalizar el resultado de G\u00f6del en lenguajes inform\u00e1ticos apropiados y luego utilizar paquetes de demostraci\u00f3n automatizados para que una m\u00e1quina demuestre ese resultado\u201d. <\/p>\n

As\u00ed lo confirmaban Benzm\u00fcller y Woltzenlogel en un art\u00edculo sobre su trabajo aparecido en el repositorio cient\u00edfico arXiv<\/a> : el teorema ontol\u00f3gico de G\u00f6del ha sido analizado por vez primera con un nivel de detalle sin precedentes usando herramientas inform\u00e1ticas de interpretaci\u00f3n de la sintaxis, de verificaci\u00f3n autom\u00e1tica de la consistencia de sus axiomas y definiciones; y de demostraci\u00f3n autom\u00e1tica del teorema, entre otras. <\/p>\n

Y lo curioso es que todo se ha hecho con dos MacBooks<\/a> ordinarios, unos ordenadores port\u00e1tiles de Apple, desarrollados para el uso en el hogar y en peque\u00f1as empresas. En general, el uso de computadoras para reducir el trabajo de los matem\u00e1ticos no es nuevo. En concreto, la demostraci\u00f3n autom\u00e1tica de teoremas (ATP<\/a>, por Automated theorem proving<\/em>) o Deducci\u00f3n automatizada<\/em>, es actualmente el subcampo m\u00e1s desarrollado del razonamiento automatizado<\/a>.<\/p>\n<\/p><\/div>\n

<\/div>\n<\/p><\/div>\n


<\/p>\n

\n
\"El <\/p>\n
El presente trabajo ayudar\u00e1 a impulsar la filosof\u00eda te\u00f3rica asistida por ordenador, esperan sus autores. Imagen: MacBook. Fuente: Apple.<\/div>\n<\/p><\/div>\n
\n
Benzm\u00fcller y Woltzenlogel han explicado a Tendencias21<\/em> en la siguiente entrevista los detalles de su investigaci\u00f3n:  <\/p>\n

\u00bfEn qu\u00e9 consiste exactamente el sistema que han utilizado para probar el teorema de G\u00f6del?<\/b> <\/p>\n

Hemos verificado el teorema de G\u00f6del en sistemas computacionales est\u00e1ndar, con herramientas de software espec\u00edficas, denominadas probadores de teoremas<\/a>\u200e y model finders<\/em>. Para ello, Bruno Woltzenlogel us\u00f3 un MacBookPro 2GHz Intel Core i7 8GB, y yo un MacBook 2.4GHz Intel Core 2 Duo y 2 GB. <\/p>\n

En nuestros experimentos tambi\u00e9n hemos hecho consultas remotas a probadores de teoremas instalados y mantenidos por la iniciativa SystemOnTPTP<\/a> de Geoff Sutcliffe. Estas consultas remotas son muy \u00fatiles, pues permiten evitar la localidad de las instalaciones de los probadores de teoremas. La especificaci\u00f3n de los ordenadores de SystemOnTPTP en Miami es: i686 Intel(R) Xeon(R) CPU 5140 @ 2.33GHz, NumberOfCPUs: 4, RAMPerCPU: 1006.25MB, OS: Linux 2.6.32.26. <\/p>\n

\u00bfCu\u00e1l ser\u00eda la diferencia entre estos sistemas y otros de razonamiento automatizado?<\/b> <\/p>\n

Las herramientas de razonamiento que usamos en este caso son capaces de razonar con una l\u00f3gica cl\u00e1sica de primer orden con gran capacidad expresiva. Eso result\u00f3 esencial en la formalizaci\u00f3n, la verificaci\u00f3n y la automatizaci\u00f3n de la prueba de G\u00f6del sobre la existencia de Dios. <\/p>\n

La mayor\u00eda de otros sistemas de razonamiento automatizado, por el contrario, se centran en partes de la l\u00f3gica de predicados de primer orden (por ejemplo, en la l\u00f3gica proposicional), lo cual resulta menos expresivo, aunque sea m\u00e1s sencillo de gestionar. <\/p>\n

\u00bfPor qu\u00e9 escogieron el teorema de G\u00f6del para su investigaci\u00f3n?<\/b> <\/p>\n

En realidad por varias razones. Por un lado, el teorema de G\u00f6del es un est\u00e1ndar de comparaci\u00f3n para probar los l\u00edmites de nuestras propias herramientas de razonamiento automatizado. Su formalizaci\u00f3n requiere de una l\u00f3gica modal de primer orden para distinguir entre una verdad \u201cposible\u201d y una verdad \u201cnecesaria\u201d. Con nuestro trabajo quer\u00edamos demostrar que el razonamiento en una l\u00f3gica modal de primer orden puede ser reducido elegante y efectivamente a un razonamiento l\u00f3gico de primer orden cl\u00e1sico. <\/p>\n

Por otra parte, el teorema de G\u00f6del es muy interesante desde el punto de vista filos\u00f3fico y es objeto de continuas investigaciones. <\/p>\n

\u00bfQu\u00e9 opinan de las implicaciones filos\u00f3ficas y religiosas que algunos medios de comunicaci\u00f3n han resaltado de su trabajo? \u00bfRealmente demuestra \u00e9ste la existencia de Dios?<\/b> <\/p>\n

El teorema de G\u00f6del depende de axiomas y de definiciones. En concreto, G\u00f6del defini\u00f3 a Dios como un ser que posee todas las propiedades positivas. Propuso cinco axiomas que describen lo que son las propiedades positivas, y se\u00f1al\u00f3 que la necesaria existencia de Dios pod\u00eda inferirse a partir de esos axiomas. En nuestro trabajo hemos verificado esa afirmaci\u00f3n de forma automatizada. <\/p>\n

Eso simplemente supone que el teorema de G\u00f6del (la necesaria existencia de Dios) debe ser cierto en nuestro mundo, si los cinco axiomas tambi\u00e9n son verdaderos. Sin embargo, la veracidad de dichos axiomas es cuestionable y no emp\u00edricamente comprobable. <\/p>\n

\u00bfPor qu\u00e9 usaron el MacBook para sus an\u00e1lisis?<\/b> <\/p>\n

Cualquier otro port\u00e1til con una configuraci\u00f3n de hardware similar y un sistema operativo moderno habr\u00eda bastado. Simplemente, somos usuarios de Mac. <\/p>\n

Sin embargo, a los medios parece haberles gustado este hecho, y han provocado una reacci\u00f3n en cadena que lo ha convertido en titular. Nos ha divertido mucho este mecanismo de propagaci\u00f3n medi\u00e1tica. <\/p>\n

Entonces, para conseguir una mejora del sistema utilizado, \u00bfse requerir\u00edan ordenadores m\u00e1s avanzados?<\/b> <\/p>\n

Un hardware m\u00e1s potente permitir\u00eda a nuestros sistemas de software operar m\u00e1s r\u00e1pidamente y manejar espacios de b\u00fasqueda m\u00e1s amplios (la prueba de un teorema es un proceso de b\u00fasqueda). <\/p>\n

En consecuencia, existe una peque\u00f1a posibilidad de que con un sistema m\u00e1s avanzado se pudieran comprobar algunos teoremas que no pueden demostrarse con un PC est\u00e1ndar. Sin embargo, la experiencia nos dice que ser\u00eda m\u00e1s inteligente invertir en mejorar las herramientas de software y su teor\u00eda subyacente que en ordenadores m\u00e1s r\u00e1pidos. <\/p>\n

\u00bfQu\u00e9 teoremas podr\u00edan analizarse con esos otros sistemas? \u00bfPlanean aplicarlos a teoremas m\u00e1s complejos?<\/b> <\/p>\n

La l\u00f3gica modal de primer orden tiene muchas aplicaciones potenciales, por ejemplo, en inteligencia artificial, ling\u00fc\u00edstica computacional o verificaci\u00f3n formal de sistemas de hardware y software. Pero la t\u00e9cnica que hemos aplicado propicia la automatizaci\u00f3n de otras l\u00f3gicas desafiantes (y de sus combinaciones), para las cuales no existen actualmente probadores. Queremos explorar esta variedad de posibilidades en el futuro. <\/p>\n

A corto plazo, tenemos intenci\u00f3n de centrarnos en pruebas ontol\u00f3gicas y queremos analizar las cr\u00edticas y las adaptaciones de la prueba de G\u00f6del con nuestra tecnolog\u00eda. A partir de este trabajo, nos gustar\u00eda contribuir a una metodolog\u00eda y a una infraestructura que apoye lo que nosotros llamamos una \u201cfilosof\u00eda te\u00f3rica asistida por ordenador\u201d. <\/p>\n

\u00bfQu\u00e9 ventajas cient\u00edficas pueden obtenerse de este avance?<\/b> <\/p>\n

Las herramientas para probar teoremas que empleamos garantizan una mayor precisi\u00f3n. Este nivel de precisi\u00f3n no se encuentra normalmente en pruebas humanas, ni siquiera en las de los presupuestos de G\u00f6del. <\/p>\n

Por ejemplo, en nuestro trabajo los par\u00e1metros de la l\u00f3gica modal de primer orden que hemos empleado son conocidos con exactitud, algo que a menudo no sucede con los documentos filos\u00f3ficos. <\/p>\n

Adem\u00e1s, algunas tareas de razonamiento, como llenar lagunas en bocetos de prueba o encontrar contra-modelos para conjeturas err\u00f3neas, pueden apoyarse ahora eficazmente con computadoras. Esperamos que en un futuro pr\u00f3ximo los fil\u00f3sofos sean preparados para utilizar nuestras herramientas, y as\u00ed mejorar su precisi\u00f3n y su eficiencia.<\/p>\n<\/p><\/div>\n<\/p><\/div>\n<\/p><\/div>\n<\/p><\/div>\n","protected":false},"excerpt":{"rendered":"

Cient\u00edficos demuestran con dos port\u00e1tiles la utilidad del razonamiento automatizado, tanto para la especulaci\u00f3n humana como para la inteligencia artificial.<\/p>\n","protected":false},"author":3,"featured_media":30197,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"advanced_seo_description":"","jetpack_seo_html_title":"","jetpack_seo_noindex":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[76],"tags":[],"class_list":["post-30198","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-actualidad"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"https:\/\/sosuaonline.net\/inicio\/wp-content\/uploads\/2013\/11\/sosua_images_dios_segun_las_computadoras.jpg","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/sosuaonline.net\/inicio\/wp-json\/wp\/v2\/posts\/30198","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/sosuaonline.net\/inicio\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/sosuaonline.net\/inicio\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/sosuaonline.net\/inicio\/wp-json\/wp\/v2\/users\/3"}],"replies":[{"embeddable":true,"href":"https:\/\/sosuaonline.net\/inicio\/wp-json\/wp\/v2\/comments?post=30198"}],"version-history":[{"count":0,"href":"https:\/\/sosuaonline.net\/inicio\/wp-json\/wp\/v2\/posts\/30198\/revisions"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/sosuaonline.net\/inicio\/wp-json\/wp\/v2\/media\/30197"}],"wp:attachment":[{"href":"https:\/\/sosuaonline.net\/inicio\/wp-json\/wp\/v2\/media?parent=30198"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/sosuaonline.net\/inicio\/wp-json\/wp\/v2\/categories?post=30198"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/sosuaonline.net\/inicio\/wp-json\/wp\/v2\/tags?post=30198"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}