{"id":18993,"date":"2018-03-09T09:07:48","date_gmt":"2018-03-09T09:07:48","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/teoria-computacional-en-acl2-sobre-calculos-proposicionales\/"},"modified":"2018-03-09T09:07:48","modified_gmt":"2018-03-09T09:07:48","slug":"teoria-computacional-en-acl2-sobre-calculos-proposicionales","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/matematicas\/teoria-computacional-en-acl2-sobre-calculos-proposicionales\/","title":{"rendered":"Teor\u00eda computacional (en acl2) sobre c\u00e1lculos proposicionales"},"content":{"rendered":"<h2>Tesis doctoral de <strong> Francisco Jes\u00fas Mart\u00edn Mateos <\/strong><\/h2>\n<p>En este trabajo se desarrolla una formalizaci\u00f3n de sistemas de razonamiento proposicionales y se verifican autom\u00e1ticamente sus principales propiedades en el sistema de demostraci\u00f3n autom\u00e1tica acl2. Tambi\u00e9n se analizan las caracter\u00edsticas comunes a determinados c\u00e1lculos bien conocidos, definiendo un marco gen\u00e9rico del que son casos particulares.  el trabajo comienza con la formalizaci\u00f3n de la l\u00f3gica proposicional, para la que se consideran dos sem\u00e1nticas, la cl\u00e1sica y la sem\u00e1ntica trivalorada fuerte de kleene. Una vez hecho esto, se desarrollan procedimientos de decisi\u00f3n de satisfacibilidad, validez y consecuencia l\u00f3gica (tanto en la sem\u00e1ntcia cl\u00e1sica como en la de kleene) basados en el c\u00e1lculo de los tableros sem\u00e1nticos y el c\u00e1lculo de secuentes. Se proporcionan implementaciones verificadas de estos procedimientos.  a partir de estos dos m\u00e9todos de decisi\u00f3n de satisfacibilidad se define un marco gen\u00e9rico que abstrae sus caracter\u00edsticas comunes: los sistemas de transformaci\u00f3n proposicionales. Esta abstracci\u00f3n permite desarrollar procedimientos de decisi\u00f3n de satisfacibilidad a partir de un conjunto de reglas de transformaci\u00f3n con determinadas propiedades b\u00e1sicas. La implementaci\u00f3n del marco gen\u00e9rico se puede instanciar para construir de forma autom\u00e1tica procedimientos verificados de decisi\u00f3n de satisfacibilidad. Se muestra c\u00f3mo se realiza esta instancia para los m\u00e9todos basados en tableros sem\u00e1nticos y en secuentes. El desarrollo del marco gen\u00e9rico se ha realizado tanto para la sem\u00e1ntica cl\u00e1sica como para la sem\u00e1ntcia de kleene.  a continuaci\u00f3n se estudian otros procedimientos de decisi\u00f3n de satisfacibilidad, analizando la posibilidad de expresarlos como sistemas de transformaci\u00f3n proposicionales. Esto ocurre con el procedimiento de davis y putnam, el cual es desarrollado primero de forma independiente al marco gen\u00e9rico y despu\u00e9s se expresa como una instancia del mismo. Este desarrollo se reali<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Teor\u00eda computacional (en acl2) sobre c\u00e1lculos proposicionales<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Teor\u00eda computacional (en acl2) sobre c\u00e1lculos proposicionales <\/li>\n<li><strong>Autor:<\/strong>\u00a0 Francisco Jes\u00fas Mart\u00edn Mateos <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Sevilla<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 17\/09\/2002<\/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>Jos\u00e9 Antonio Alonso Jimenez<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: eladio Dom\u00ednguez murillo <\/li>\n<li>julio Jes\u00fas Rubio Garc\u00eda (vocal)<\/li>\n<li>agust\u00edn Riscos fern\u00e1ndez (vocal)<\/li>\n<li>joaqu\u00edn Borrego d\u00edaz (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Francisco Jes\u00fas Mart\u00edn Mateos En este trabajo se desarrolla una formalizaci\u00f3n de sistemas de razonamiento proposicionales y [&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":[15608,3183,58580,1890,2528,3747,3748,13456,126,10715],"tags":[58582,10833,58581,10817,10822,10901],"class_list":["post-18993","post","type-post","status-publish","format-standard","hentry","category-analisis-combinatorio","category-analisis-y-analisis-funcional","category-calculo-proposicional","category-ciencia-de-los-ordenadores","category-inteligencia-artificial","category-logica","category-logica-deductiva","category-logica-formal","category-matematicas","category-sevilla","tag-agustin-riscos-fernandez","tag-eladio-dominguez-murillo","tag-francisco-jesus-martin-mateos","tag-joaquin-borrego-diaz","tag-jose-antonio-alonso-jimenez","tag-julio-jesus-rubio-garcia"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/18993","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=18993"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/18993\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=18993"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=18993"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=18993"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}