{"id":30620,"date":"2004-09-06T00:00:00","date_gmt":"2004-09-06T00:00:00","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/teoria-computacional-en-pvs-de-la-programacion-logica-y-del-analisis-formal-de-conceptos\/"},"modified":"2004-09-06T00:00:00","modified_gmt":"2004-09-06T00:00:00","slug":"teoria-computacional-en-pvs-de-la-programacion-logica-y-del-analisis-formal-de-conceptos","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/sevilla\/teoria-computacional-en-pvs-de-la-programacion-logica-y-del-analisis-formal-de-conceptos\/","title":{"rendered":"Teoria computacional (en pvs) de la programaci\u00f3n logica y del analisis formal de conceptos"},"content":{"rendered":"<h2>Tesis doctoral de <strong> Mar\u00eda  Jose Hidalgo Doblado <\/strong><\/h2>\n<p>Los objetivos principales de la tesis son la formalizaci\u00f3n de teor\u00edas matem\u00e1ticas en sistemas de razonamiento autom\u00e1tico, la verificaci\u00f3n formal de algoritmos de dichas teor\u00edas y la realizaci\u00f3n de dicha verificaci\u00f3n de forma que las pruebas en el sistema se correspondan esencialmente con las habituales. para ello, hemos elegido un sistema de razonamiento, pvs, y dos teor\u00edas como objetos de formalizaci\u00f3n, la programaci\u00f3n l\u00f3gica preposicional y el an\u00e1lisis formal de conceptos. por otra parte, el deseo de realizar un razonamiento natural sobre las especificaciones conduce al problema de la elecci\u00f3n de los tipos b\u00e1sicos sobre los que construir las especificaciones. En este sentido, los tipos de datos elegidos para representar formalmente las nociones de las teor\u00edas han de estar los m\u00e1s pr\u00f3ximo posible a dichas nociones. En ambos casos, el tipo m\u00e1s cercano al os objetos que se desea representar en el lenguaje de pvs es el tipo de los conjuntos finitos. ahora bien, aunque la elecci\u00f3n del tipo de los conjuntos de pvs como tipo base para realizar las especificaciones haga posible un razonamiento elegante sobre las mismas, se tiene el problema de que dichas especificaciones no son evaluables. La soluci\u00f3n que proponemos para este problema es de car\u00e1cter metodol\u00f3gico. Para ello hemos establecido en pvs un marco gen\u00e9rico en el que relacionar distintas especificaciones, definiendo formalmente cu\u00e1ndo dos especificaciones diferentes corresponden a un mismo concepto.  en dicho marco, hemos estudiado las propiedades de car\u00e1cter general que se conservan entre especificaciones de un mismo algoritmo. Esto nos ha permitido trabajar en dos planos. Por una parte, realizar el razonamiento en el plano en el que la distancia entre una noci\u00f3n y su especificaci\u00f3n formal es m\u00ednima, aunque \u00e9sta no sea evaluable. Y por otra, s\u00f3lo para determinadas especificaciones, obtener otras evaluables correspondientes al mismo concepto, y con las mismas propiedades (en par<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Teoria computacional (en pvs) de la programaci\u00f3n logica y del analisis formal de conceptos<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Teoria computacional (en pvs) de la programaci\u00f3n logica y del analisis formal de conceptos <\/li>\n<li><strong>Autor:<\/strong>\u00a0 Mar\u00eda  Jose Hidalgo Doblado <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Sevilla<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 09\/06\/2004<\/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>agustin Riscos fernandez (vocal)<\/li>\n<li>alejandro Fern\u00e1ndez margarit (vocal)<\/li>\n<li>julio Jes\u00fas Rubio Garc\u00eda (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Mar\u00eda Jose Hidalgo Doblado Los objetivos principales de la tesis son la formalizaci\u00f3n de teor\u00edas matem\u00e1ticas en [&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":[10715],"tags":[58582,10818,10822,10901,10819,85937],"class_list":["post-30620","post","type-post","status-publish","format-standard","hentry","category-sevilla","tag-agustin-riscos-fernandez","tag-alejandro-fernandez-margarit","tag-jose-antonio-alonso-jimenez","tag-julio-jesus-rubio-garcia","tag-luis-maria-laita-de-la-rica","tag-maria-jose-hidalgo-doblado"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/30620","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=30620"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/30620\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=30620"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=30620"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=30620"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}