{"id":13027,"date":"2018-03-09T08:59:08","date_gmt":"2018-03-09T08:59:08","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/una-teoria-computacional-acerca-de-la-logica-ecuacional-formalizacion-en-acl2-de-la-logica-ecuacional-y-demostracion-automatica-de-sus-propiedades\/"},"modified":"2018-03-09T08:59:08","modified_gmt":"2018-03-09T08:59:08","slug":"una-teoria-computacional-acerca-de-la-logica-ecuacional-formalizacion-en-acl2-de-la-logica-ecuacional-y-demostracion-automatica-de-sus-propiedades","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/matematicas\/una-teoria-computacional-acerca-de-la-logica-ecuacional-formalizacion-en-acl2-de-la-logica-ecuacional-y-demostracion-automatica-de-sus-propiedades\/","title":{"rendered":"Una teoria computacional acerca de la logica ecuacional (formalizacion en acl2 de la logica ecuacional y demostracion automatica de sus propiedades)"},"content":{"rendered":"<h2>Tesis doctoral de <strong> Jos\u00e9 Luis Ruiz Reina <\/strong><\/h2>\n<p>El objetivo principal de la tesis es el desarrollo de una teoria computacional acerca de la logica ecuacional, usando para ello el sistema acl2. Es decir, se usa acl2 para definir formalmente algoritmos y conceptos relacionados con la l\u00f3gica ecuacional, y se llevan a cabo demostraciones autom\u00e1ticas de teoremas acerca de estos algoritmos y conceptos. Este trabajo de verificaci\u00f3n formal se realiza en un entorno en el que se pueden combinar la demostraci\u00f3n de teoremas con la ejecuci\u00f3n de funciones.  la teoria desarrollada se estructura en tres bloques:  -propiedades de los terminos de primer orden y su estructura de reticulo respecto de la relacion de subsuncion.  -reducciones abstractas.  -teorias ecuacionales y sistemas de reescritura de terminos  de entre los teoremas demostrados autom\u00e1ticamente cabe destacar la verificacion formal de un algoritmo de unificacion, el lema de newman para reducciones abstractas y el teorema de pares criticos de knuth y bendix.<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Una teoria computacional acerca de la logica ecuacional (formalizacion en acl2 de la logica ecuacional y demostracion automatica de sus propiedades)<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Una teoria computacional acerca de la logica ecuacional (formalizacion en acl2 de la logica ecuacional y demostracion automatica de sus propiedades) <\/li>\n<li><strong>Autor:<\/strong>\u00a0 Jos\u00e9 Luis Ruiz Reina <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Sevilla<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 28\/09\/2001<\/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: Luis Mar\u00eda Laita de la rica <\/li>\n<li>robert lukas mario Nieuwenhuis (vocal)<\/li>\n<li>alejandro Fernandez margarit (vocal)<\/li>\n<li>albert Rubio gimeno (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Jos\u00e9 Luis Ruiz Reina El objetivo principal de la tesis es el desarrollo de una teoria computacional [&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,10816,126,10715,6566],"tags":[15920,10818,10822,42415,10819,6477],"class_list":["post-13027","post","type-post","status-publish","format-standard","hentry","category-ciencia-de-los-ordenadores","category-inteligencia-artificial","category-logica","category-logica-deductiva","category-logica-matematica","category-matematicas","category-sevilla","category-sistemas-formales","tag-albert-rubio-gimeno","tag-alejandro-fernandez-margarit","tag-jose-antonio-alonso-jimenez","tag-jose-luis-ruiz-reina","tag-luis-maria-laita-de-la-rica","tag-robert-lukas-mario-nieuwenhuis"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/13027","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=13027"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/13027\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=13027"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=13027"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=13027"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}