Presentación de sistemas de razonamiento

Esta semana se ha celebrado un curso en la Facultad de Matemáticas sobre Software libre frente a software comercial: posibilidades y aplicaciones a la docencia. Dentro del curso hice una presentación de sistemas de razonamiento automático. En la presentación comento brevemente cómo trabajar con distintos sistemas de razonamiento (Otter/MACE, ACL2, PVS e Isabelle/Isar) usados por nuestro grupo y algunas aplicaciones de los distintos sistemas.