{"id":40126,"date":"1999-01-01T00:00:00","date_gmt":"1999-01-01T00:00:00","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/delta-arboles-de-implicantes-e-implicados-y-reducciones-de-logicas-en-atps\/"},"modified":"1999-01-01T00:00:00","modified_gmt":"1999-01-01T00:00:00","slug":"delta-arboles-de-implicantes-e-implicados-y-reducciones-de-logicas-en-atps","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/logica\/delta-arboles-de-implicantes-e-implicados-y-reducciones-de-logicas-en-atps\/","title":{"rendered":"Delta-arboles de implicantes e implicados y reducciones de logicas en atps."},"content":{"rendered":"<h2>Tesis doctoral de <strong> Agustin Valverde Ramos <\/strong><\/h2>\n<p>El trabajo pertenece al campo de la demostraci\u00f3n autom\u00e1tica para las l\u00f3gicas multivaluadas, tarea que se aborda desde el estudio de la satisfacibilidad en l\u00f3gicas signadas. una de las aportaciones de la tesis es la introducci\u00f3n de las l\u00f3gicas signadas con dos enriquecimientos respecto de otras aproximaciones: se consideran m\u00e1s conectivos y se abre la sensibilidad de que las l\u00f3gicas sean reducidas.  la relaci\u00f3n entre las l\u00f3gicas multivaluadas y las l\u00f3gicas signadas se establece con las transformaciones de signado; en la tesis se estudia la eficiencia de estas transformaciones y se describe una familia (que amplia las existentes en la bibliograf\u00eda) de l\u00f3gicas signables, es decir, que admiten una transformaci\u00f3n de signado eficiente. Para el resto de las l\u00f3gicas se propone una t\u00e9cnica alternativa: el signado perezoso, aplicable a demostradores basados en simplificaciones.  en la segunda parte de la tesis construyen dos algoritmos de satisfacibilidad para l\u00f3gicas signadas dentro de la metodolog\u00eda tas. Estos algoritmos se describen mediante reducciones, transformaciones que disminuyen el tama\u00f1o, tanto de la f\u00f3rmula como de la l\u00f3gica, antes de aplicar los procesos de ramificaci\u00f3n culpables de la complejidad exponencial de estos algoritmos. Estas transformaciones hacen uso de la informaci\u00f3n que se obtiene a partir de los implicantes e implicados de las subf\u00f3rmulas de la una f\u00f3rmula dada. En el segundo demostrador se utiliza una nueva representaci\u00f3n de las f\u00f3rmulas signadas, los a-\u00e1rboles, para mejorar las transformaciones y reducir su coste computacional, debido a que se utilizan justamente los implicantes\/implicados para describir la representaci\u00f3n.<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Delta-arboles de implicantes e implicados y reducciones de logicas en atps.<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Delta-arboles de implicantes e implicados y reducciones de logicas en atps. <\/li>\n<li><strong>Autor:<\/strong>\u00a0 Agustin Valverde Ramos <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 M\u00e1laga<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 01\/01\/1999<\/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>Inmaculada Perez De Guzman Molina<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: Francisco Triguero ruiz <\/li>\n<li>Jos\u00e9 Meseguer guaita (vocal)<\/li>\n<li> Barja perez Jos\u00e9 Mar\u00eda (vocal)<\/li>\n<li> Fari\u00f1as del cerro Luis (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Agustin Valverde Ramos El trabajo pertenece al campo de la demostraci\u00f3n autom\u00e1tica para las l\u00f3gicas multivaluadas, tarea [&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":[3747,3748,10816,7834,19007],"tags":[48496,3754,6569,7838,24725,66540],"class_list":["post-40126","post","type-post","status-publish","format-standard","hentry","category-logica","category-logica-deductiva","category-logica-matematica","category-malaga","category-teoria-de-modelos","tag-agustin-valverde-ramos","tag-barja-perez-jose-maria","tag-farinas-del-cerro-luis","tag-francisco-triguero-ruiz","tag-inmaculada-perez-de-guzman-molina","tag-jose-meseguer-guaita"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/40126","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=40126"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/40126\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=40126"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=40126"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=40126"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}