Razonamiento Automático

Relaciones de ejercicios

Práctica 1: Ejercicios de formalización en APLI2

Hay que crearse una cuenta de usuario para comenzar a trabajar. Se sugiere utilizar como identificador de usuario la cadena formada por las tres primeras letras del nombre y el primer y segundo apellidos; así el identificador de Juan Diego Lopez Ruiz sería jualoprui.

Una vez se ha entrado en la aplicación APLI2, se ha de escoger la opción Formalización y aparecerá la lista de ejercicios disponibles para formalizar. Cada ejercicio consta de una serie de premisas y una conclusión, cada una de las cuales se puede formalizar pulsando sobre el icono de la lupa que los acompaña. Para comprobar si la formalización es correcta se utiliza el sistema OTTER.

Importante: No se utiliza el punto para terminar las fórmulas en la formalización.

Práctica 2: Argumentaciones en Otter
Práctica 3: Tratamiento de la igualdad en Otter
Práctica 4: Recursión e inducción en ACL2
Práctica 5: Interacción con el sistema ACL2
Práctica 6: Lógicas Temporales

Utilidades

ACL2 en Emacs: Fichero de configuración de ACL2 para Emacs. Hay que añadirlo al final del fichero de configuración de Emacs (.emacs en Linux/_emacs en Windows).
Incorpora varias funcionalidades:
  • El comando run-acl2 divide horizontalmente la ventana de Emacs en 2 dejando arriba el fichero original en el que se está trabajando y abajo comienza una sesión del sistema ACL2
  • El comando C-x C-e limpia la sesión de ACL2 y evalúa la expresión que hay delante del cursor
  • El comando C-x C-a evalúa en ACL2 todas las expresiones de un fichero desde su comienzo hasta el punto donde se encuentra el cursor