{"id":32098,"date":"1997-01-01T00:00:00","date_gmt":"1997-01-01T00:00:00","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/resolucion-sl-un-paradigma-basado-en-resolucion-lineal-para-la-demostracion-automatica\/"},"modified":"1997-01-01T00:00:00","modified_gmt":"1997-01-01T00:00:00","slug":"resolucion-sl-un-paradigma-basado-en-resolucion-lineal-para-la-demostracion-automatica","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/matematicas\/resolucion-sl-un-paradigma-basado-en-resolucion-lineal-para-la-demostracion-automatica\/","title":{"rendered":"Resolucion sl*: un paradigma basado en resolucion lineal para la demostracion automatica."},"content":{"rendered":"<h2>Tesis doctoral de <strong>  Casamayor Rodenas Juan  Carlos <\/strong><\/h2>\n<p>El trabajo incluido en la presente tesis se enmarca dentro del campo de la demostracion automatica de teoremas y consiste en el estudio, definicion y desarrollo de un paradigma de resolucion lineal, denominado resolucion sl*: la razon para utilizar la denominacion de paradigma reside en el hecho de que en si misma resolucion sl* no es un procedimiento, sino que se puede entender como una forma de razonamiento con ciertos parametros cuya instanciacion da lugar a diferentes procedimientos que son adecuados al tratamiento de distintos tipos de problemas. Por otro lado, se le ha dado el nombre de resolucion sl* porque, como posteriormente se explicara, esta muy cercano a eliminacion de modelos y a resolucion sl (de ahi la primera parte del nombre). El asterisco final quiere denotar su parametrizacion, de forma que los procedimientos instancias de resolucion sl* seran denominados con una letra mas en vez del asterisco, como posteriormente se vera.  en resolucion sl* se introduce el concepto fundamental de \u00abeleccion de ancestros\u00bb. La eleccion de ancestros es el mecanismo que permite controlar la aplicacion de la resolucion de ancestro haciendo posible una reduccion del coste de su palicacion y una adecuacion de resolucion sl* al tipo de problemas a tratar. El trabajo hace especial hincapie en la importancia de la eleccion de ancestros, ya que es la principal aportacion de resolucion sl*, analizando tanto las ventajas que aporta asociadas al incremento de la eficiencia como el hecho de dotar a resolucion sl* la capacidad de adaptarse a los problemas que trata. Tambien se presenta una implementacion de resolucion sl*, en particular del procedimiento slt, y se incluyen resultados sobre un conjunto extenso de problemas del campo de la demostracion automatica.<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Resolucion sl*: un paradigma basado en resolucion lineal para la demostracion automatica.<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Resolucion sl*: un paradigma basado en resolucion lineal para la demostracion automatica. <\/li>\n<li><strong>Autor:<\/strong>\u00a0  Casamayor Rodenas Juan  Carlos <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Polit\u00e9cnica de Valencia<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 01\/01\/1997<\/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>Isidro Ramos Salavert<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: Mario Rodr\u00edguez Artalejo <\/li>\n<li>Ambrosio Toval Alvarez (vocal)<\/li>\n<li>Jos\u00e9 Cuena Bartolome (vocal)<\/li>\n<li>Mari Alpuente Frasnedo (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Casamayor Rodenas Juan Carlos El trabajo incluido en la presente tesis se enmarca dentro del campo 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":[1890,2528,3747,3748,126,16820,6566],"tags":[17054,88854,17055,13268,88855,4813],"class_list":["post-32098","post","type-post","status-publish","format-standard","hentry","category-ciencia-de-los-ordenadores","category-inteligencia-artificial","category-logica","category-logica-deductiva","category-matematicas","category-politecnica-de-valencia","category-sistemas-formales","tag-ambrosio-toval-alvarez","tag-casamayor-rodenas-juan-carlos","tag-isidro-ramos-salavert","tag-jose-cuena-bartolome","tag-mari-alpuente-frasnedo","tag-mario-rodriguez-artalejo"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/32098","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=32098"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/32098\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=32098"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=32098"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=32098"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}