RA2010: Isabelle como un lenguaje funcional

PorJosé A. Alonso

En la clase de hoy del curso de Razonamiento automático se ha visto cómo se puede en Isabelle/HOL

  • calcular con los números naturales, los números enteros y los booleanos,
  • definir funciones mediante composición, condicionales, casos e inducción,
  • demostrar propiedades mediante simplificación,
  • definir tipos de datos recursivos,
  • definir y modificar registros y
  • refutar propiedades con QuickCheck.

Read More “RA2010: Isabelle como un lenguaje funcional”

RA2010: Visión panorámica del razonamiento automático

PorJosé A. Alonso

Hoy ha comenzado el curso de Razonamiento automático del Máster Universitario en Lógica, Computación e Inteligencia Artificial de la Universidad de Sevilla.

En la clase de hoy se ha presentado la asignatura y se ha comentado 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.
Read More “RA2010: Visión panorámica del razonamiento automático”