Teoria computacional (en PVS) de la programación logica y del analisis formal de conceptos

• Autores: María José Hidalgo Doblado
• Directores de la Tesis: José Antonio Alonso Jiménez (dir. tes.)
• Lectura: En la Universidad de Sevilla ( España ) en 2004
• Idioma: español
• Tribunal Calificador de la Tesis: Luis María Laita de la Rica (presid.) , Eugenio Roanes Lozano (secret.) , Alejandro Fernández Margarit (voc.) , Julio Rubio García (voc.) , Agustín Riscos Fernández (voc.)
• Texto completo no disponible (Saber más ...)
• Resumen

  • Los objetivos principales de la Tesis son la formalización de teorías matemáticas en sistemas de razonamiento automático, la verificación formal de algoritmos de dichas teorías y la realización de dicha verificación 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ías como objetos de formalización, la programación lógica preposicional y el análisis formal de conceptos.

    Por otra parte, el deseo de realizar un razonamiento natural sobre las especificaciones conduce al problema de la elección de los tipos básicos sobre los que construir las especificaciones. En este sentido, los tipos de datos elegidos para representar formalmente las nociones de las teorías han de estar los más próximo posible a dichas nociones. En ambos casos, el tipo más 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ón 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ón que proponemos para este problema es de carácter metodológico. Para ello hemos establecido en PVS un marco genérico en el que relacionar distintas especificaciones, definiendo formalmente cuándo dos especificaciones diferentes corresponden a un mismo concepto.

    En dicho marco, hemos estudiado las propiedades de carácter 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ón y su especificación formal es mínima, aunque ésta no sea evaluable. Y por otra, sólo para determinadas especificaciones, obtener otras evaluables correspondientes al mismo concepto, y con las mismas propiedades (en par