RA2013: Panorama del razonamiento automático mediante Prover9, ACL2, PVS e Isabelle

En la clase de hoy del curso de Razonamiento automático se presentado una visión panorámica del razonamiento automático a través de ejemplos con los sistemas de razonamiento Prover9/Mace4, ACL2, PVS e Isabelle/HOL.

Las transparencias de la clase están aquí.