DAO2012: Panorama de la demostración automática de teoremas
En la clase de hoy de Demostración asistida por ordenador se ha realizado una breve introducción a la demostración automática de teoremas a través del demostrador Prover9/Mace4 y la librería TPTP (Thousands of Problems for Theorem Provers).
Las transparencias usadas en la clase son las comprendidas entre las páginas 1 y 15 del tema 1.