DEMOSTRACIÓN DE TEOREMAS MEDIANTE LENGUAJES FUNCIONALES

Abstract

Este trabajo explora la relación entre la lógica matemática y la programación funcional, centrándose en el isomorfismo de Curry-Howard. Se analiza cómo los sistemas de demostración de Hilbert y la lógica combinatoria por un lado y los tipos algebraicos de dato y el sistema de deduccion natural por otro; pueden modelarse en Scala permitiendo formalizar demostraciones matemáticas mediante tipos y funciones. Se presentan ejemplos de teoremas lógicos implementados en código, destacando la equivalencia entre proposiciones lógicas y estructuras computacionales.