Saber UCV
Repositorio Institucional
Repositorio Institucional
Please use this identifier to cite or link to this item:
https://saber.ucv.ve/handle/10872/10358
|
| Title: | Utilización de un asistente Coq para la demostración de teoremas en la teoría de lenguajes formales y síntesis de programas |
| Authors: | Salas Oliveros, Jorge Filadelfo |
| Keywords: | Matemática Ingeniería del software |
| Issue Date: | 2008 |
| Publisher: | Anuario CDCH 2008 |
| Abstract: | Las bases fundamentales de este proyecto son las técnicas novedosas existentes en el campo de la demostración semiautomática de teoremas. En particular se utilizaron herramientas como la inducción por reescritura y el asistente de pruebas Coq. Aplica con éxito estas herramientas en la prueba de teoremas de lenguajes formales como fragmento implicativo de la lógica intuicionista. Además, logra procesar el término del cálculo de construcciones, sintetizado a partir de la prueba en Coq para transformarlo en un término del cálculo lambda a partir del cual es posible reconstruir el árbol en prueba del teorema inicial, utilizando algoritmos que programa en el lenguaje Haskell. Concluye que el área de la ciencia de computación cobra cada día mayor importancia en la automatización de los procesos de demostración y verificación de teoremas como una herramienta confiable en la ingeniería del software. |
| URI: | http://hdl.handle.net/10872/10358 |
| ISSN: | 18565891 |
| Appears in Collections: | Proyectos CDCH |
Files in This Item:
|
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.