RA2019: Ejercicios de cuantificadores sobre listas en Isabelle/HOL

En la segunda parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de la 4ª relación de ejercicios de cuantificadores sobre listas. Para cada propiedad se dan tres demostraciones en Isabelle/HOL: la primera automática, la segunda estructurada y la tercera totalmente detallada mostrando todos los lemas de HOL que se utilizan en cada paso.

La teoría con las soluciones de los ejercicios es la siguiente
Read More “RA2019: Ejercicios de cuantificadores sobre listas en Isabelle/HOL”

RA2019: Razonamiento sobre árboles y bosques en Isabelle/HOL

En la primera parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo definir y razonar en Isabelle/HOL tipos de datos recursivos como árboles binarios, árboles generales y bosques. En su definición se usa recursión cruzada y en la demostración de sus propiedades se usa inducción doble.

La teoría utilizada es la siguiente
Read More “RA2019: Razonamiento sobre árboles y bosques en Isabelle/HOL”

I1M2019: Programa en Haskell para reconocer tautologías

En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado cómo construir un programa para determinar si una fórmula es una tautología.

Para ello se consideran las siguientes fases:

  1. definir un tipo de dato algebraico para las fórmulas proposicionales,
  2. definir un tipo de dato para las interpretaciones,
  3. definir una función para calcular los valores de las fórmulas en las interpretaciones
  4. definir una función para generar todas las posibles interpretaciones de una fórmula y
  5. definir una función que para decidir si una fórmula es tautología (es decir, su valor es verdadero en todas sus interpretaciones).

Los apuntes correspondientes a la clase son

Una versión interactiva de los apuntes en IHaskell se encuentra aquí.