SABER UCV >
1) Investigación >
Proyectos CDCH >
Por favor, use este identificador para citar o enlazar este ítem:
http://hdl.handle.net/10872/10358
|
Título : | Utilización de un asistente Coq para la demostración de teoremas en la teoría de lenguajes formales y síntesis de programas |
Autor : | Salas Oliveros, Jorge Filadelfo |
Palabras clave : | Matemática Ingeniería del software |
Fecha de publicación : | 2008 |
Editorial : | Anuario CDCH 2008 |
Resumen : | 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 |
Aparece en las colecciones: | Proyectos CDCH
|
Los ítems de DSpace están protegidos por copyright, con todos los derechos reservados, a menos que se indique lo contrario.
|