RA2011: Panorama del razonamiento automático mediante Otter, 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 Otter/Mace, ACL2, PVS e Isabelle/HOL.

Las transparencias de la clase son