Tesis Doctoral
Una teoría computacional acerca de la lógica ecuacional formalización en ACL2 de la lógica ecuacional y demostración automática de sus propiedades
Autor/es | Ruiz Reina, José Luis |
Director | Alonso Jiménez, José Antonio |
Departamento | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Fecha de publicación | 2001 |
Fecha de depósito | 2015-04-16 |
Resumen | El objetivo principal de la Tesis es el desarrollo de una teoría computacional acerca de la lógica ecuacional, usando para ello el sistema ACL2. Es decir, se usa ACL2 para definir formalmente algoritmos y conceptos ... El objetivo principal de la Tesis es el desarrollo de una teoría computacional acerca de la lógica ecuacional, usando para ello el sistema ACL2. Es decir, se usa ACL2 para definir formalmente algoritmos y conceptos relacionados con la lógica ecuacional, y se llevan a cabo demostraciones automáticas de teoremas acerca de estos algoritmos y conceptos. Este trabajo de verificación formal se realiza en un entorno en el que se pueden combinar la demostración de teoremas con la ejecución de funciones.| |
Cita | Ruiz Reina, J.L. (2001). Una teoría computacional acerca de la lógica ecuacional formalización en ACL2 de la lógica ecuacional y demostración automática de sus propiedades. (Tesis Doctoral Inédita). Universidad de Sevilla, Sevilla. |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
C_043-373.pdf | 19.12Mb | [PDF] | Ver/ | |