Utilización de un asistente Coq para la demostración de teoremas en la teoría de lenguajes formales y síntesis de programas

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.