RA2018: Razonamiento automático con Coq

En la clase de hoy del curso de Razonamiento automático se ha explicado cómo se puede usar Coq como alternativa a Isabelle/HOL que hemos utilizado anteriormente en el curso.

Los temas, con las correspondientes teorías de Coq, que se han explicado
son:

• Programación funcional y métodos elementales de demostración en Coq.
• Demostraciones por inducción sobre los números naturales en Coq.
• Datos estructurados en Coq.
• Polimorfismo y funciones de orden superior en Coq.
• Tácticas básicas de Coq.
• Lógica en Coq.