SABER UCV >
1) Investigación >
Proyectos CDCH >

Por favor, use este identificador para citar o enlazar este ítem: http://hdl.handle.net/123456789/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://saber.ucv.ve/jspui/handle/123456789/10358
ISSN : 18565891
Aparece en las colecciones: Proyectos CDCH

Ficheros en este ítem:

Fichero Descripción Tamaño Formato
Utilización de un asistente Coq para la demostración de teoremas en la teoría de lenguajes formales y síntesis de programas.pdf107.21 kBAdobe PDFVisualizar/Abrir

Los ítems de DSpace están protegidos por copyright, con todos los derechos reservados, a menos que se indique lo contrario.

 

Valid XHTML 1.0! DSpace Software Copyright © 2002-2008 MIT and Hewlett-Packard - Comentarios