{"id":79411,"date":"2006-04-04T00:00:00","date_gmt":"2006-04-04T00:00:00","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/razonamiento-mecanizado-en-algebra-homologica\/"},"modified":"2006-04-04T00:00:00","modified_gmt":"2006-04-04T00:00:00","slug":"razonamiento-mecanizado-en-algebra-homologica","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/sistemas-formales\/razonamiento-mecanizado-en-algebra-homologica\/","title":{"rendered":"Razonamiento mecanizado en \u00e1lgebra homol\u00f3gica"},"content":{"rendered":"<h2>Tesis doctoral de <strong> Jes\u00fas Mar\u00eda Aransay Azofra <\/strong><\/h2>\n<p>En la tesis se aborda el problema de obtener una versi\u00f3n certificada de un algoritmo fundamental en topolog\u00eda algebraica, conocido como \u00ablema b\u00e1sico de perturbaci\u00f3n\u00bb. Dicho resultado es una pieza central del sistema kenzo, software dedicado al c\u00e1lculo simb\u00f3lico en topolog\u00eda algebraica. Para tal fin, se utiliza el asistente de demostraci\u00f3n isabelle. el contenido de la tesis est\u00e1 dividido en cinco cap\u00edtulos. En el primero, se realiza una breve introducci\u00f3n a las herramientas de trabajo utilizadas. En este caso, se dan algunas definiciones y resultados en el \u00e1rea del \u00e1lgebra homol\u00f3gica, as\u00ed como informaciones relevantes sobre el sistema de c\u00e1lculo simb\u00f3lico kenzo y sobre el demostrador de teoremas isabelle. En el segundo cap\u00edtulo, se enuncia el lema de perturbaci\u00f3n b\u00e1sico y se da una demostraci\u00f3n formal del mismo, basada en una demostraci\u00f3n de f.Sergeraert. El tercer cap\u00edtulo presenta la mayor parte de los resultados que se han obtenido de la investigaci\u00f3n realizada. Dichos resultados van en la direcci\u00f3n de la modelizaci\u00f3n, especificaci\u00f3n y verificaci\u00f3n de enunciados matem\u00e1ticos en el demostrador de teoremas isabelle. M\u00e1s concretamente, se proponen y analizan desde distintos puntos de vista (que abarcan desde la especificaci\u00f3n formal hasta la automatizaci\u00f3n de resultados), cuatro representaciones distintas de los objetos matem\u00e1ticos necesarios en las demostraciones. Una de estas representaciones es escogida finalmente por satisfacer los requisitos demandados. En el cuarto cap\u00edtulo se hace una una propuesta de extracci\u00f3n de programas certificados desde isabelle. El inter\u00e9s de esta propuesta es doble: en primer lugar, su originalidad, ya que evita restringir las demostraciones matem\u00e1ticas a l\u00f3gicas constructivas. En segundo lugar, la aplicabilidad al tipo de enunciados que se pretende abordar, que la hace especialmente atractiva para los programas y enunciados en los que se basa kenzo. En el quinto cap\u00edtulo se enuncian las conclusi<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Razonamiento mecanizado en \u00e1lgebra homol\u00f3gica<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Razonamiento mecanizado en \u00e1lgebra homol\u00f3gica <\/li>\n<li><strong>Autor:<\/strong>\u00a0 Jes\u00fas Mar\u00eda Aransay Azofra <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Rioja<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 04\/04\/2006<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<h3>Direcci\u00f3n y tribunal<\/h3>\n<ul>\n<li><strong>Director de la tesis<\/strong>\n<ul>\n<li>Julio Jes\u00fas Rubio Garc\u00eda<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: eladio Dom\u00ednguez murillo <\/li>\n<li>renaud Rioboo (vocal)<\/li>\n<li>Luis Espa\u00f1ol gonz\u00e1lez (vocal)<\/li>\n<li>francis Sergeraert (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Jes\u00fas Mar\u00eda Aransay Azofra En la tesis se aborda el problema de obtener una versi\u00f3n certificada de [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"site-sidebar-layout":"default","site-content-layout":"","ast-site-content-layout":"","site-content-style":"default","site-sidebar-style":"default","ast-global-header-display":"","ast-banner-title-visibility":"","ast-main-header-display":"","ast-hfb-above-header-display":"","ast-hfb-below-header-display":"","ast-hfb-mobile-header-display":"","site-post-title":"","ast-breadcrumbs-content":"","ast-featured-img":"","footer-sml-layout":"","theme-transparent-header-meta":"","adv-header-id-meta":"","stick-header-meta":"","header-above-stick-meta":"","header-main-stick-meta":"","header-below-stick-meta":"","astra-migrate-meta-layouts":"default","ast-page-background-enabled":"default","ast-page-background-meta":{"desktop":{"background-color":"var(--ast-global-color-4)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"ast-content-background-meta":{"desktop":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"footnotes":""},"categories":[28669,13880,18890,6566],"tags":[10833,41937,170450,10901,61657,170451],"class_list":["post-79411","post","type-post","status-publish","format-standard","hentry","category-homologia","category-informatica","category-rioja","category-sistemas-formales","tag-eladio-dominguez-murillo","tag-francis-sergeraert","tag-jesus-maria-aransay-azofra","tag-julio-jesus-rubio-garcia","tag-luis-espanol-gonzalez","tag-renaud-rioboo"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/79411","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/comments?post=79411"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/79411\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=79411"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=79411"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=79411"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}