LMF2014: Deducción natural proposicional en Isabelle/HOL

PorJosé A. Alonso

En la clase de hoy del curso Lógica matemática y fundamentos se ha completado la formalización en Isabelle/HOL de las demostraciones por deducción natural estudiadas en el tema 2.

Para cada uno de los ejemplos se ha presentado distintas demostraciones: detallada (que sea parecida a la mostrada en las transparencias), estructurada y automática.

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “LMF2014: Deducción natural proposicional en Isabelle/HOL”

I1M2013: Combinatoria en Haskell

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas se han explicado las soluciones de los ejercicios de la relación 21.

El objetivo de esta relación es estudiar la generación y el número de las principales operaciones de la combinatoria. En concreto, se estudia

  • Permutaciones.
  • Combinaciones sin repetición..
  • Combinaciones con repetición
  • Variaciones sin repetición.
  • Variaciones con repetición.

Además, se estudia dos temas relacionados:

  • Reconocimiento y generación de subconjuntos y
  • El triángulo de Pascal

Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2013: Combinatoria en Haskell”