DAO2011: Panorama del razonamiento automático a través de Prover9, ACL2, PVS e Isabelle

En la clase de hoy del curso de Demostración asistida por ordenador (DAO2011) se ha realizado una presentación del razonamiento automático mostrando ejemplos de razonamiento asistido por los siguientes sistemas: Prover9, ACL2, PVS e Isabelle. Además, se ha comentado las principales aplicaciones desarrolladas en cada uno de ellos.

Las transparencias utilizadas, con los correspondientes enlaces, son las que se muestran a continuación: