DAO2011: Isabelle como un lenguaje funcional

En la clase de hoy del curso de Demostración asistida por ordenador (DAO2011) se ha presentado Isabelle como un sistema de programación funcional que permite

  • evaluar expresiones aritméticas y lógicas (con value),
  • definir funciones no recursivas (con definition),
  • definir funciones recursivas (con primrec),
  • enunciar propiedades (con lemma),
  • demostrar propiedades por simplificación (con simp) y
  • demostrar propiedades por inducción (con induct y auto).

La teoría correspondiente a la clase es Tema_1.thy cuyo contenido se muestra a continuación
Read More “DAO2011: Isabelle como un lenguaje funcional”

I1M2010: Los problemas de las reinas y de Hamming en Haskell

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos vistos otras dos aplicaciones de la programación funcional en Haskell: el problema de las reinas (consistente en colocar N reinas en un tablero de dimensiones N por N de forma que no se encuentren más de una en la misma línea: horizontal, vertical o diagonal) y el problema de Hamming (consistente definir una sucesión estrictamente creciente de números tales que el número 1 está en la sucesión y que, si x está en la sucesión, entonces 2*x, 3*x y 5*x también están).

Las transparencias usadas en la clase son desde la página 37 a la 45 del tema 11:
Read More “I1M2010: Los problemas de las reinas y de Hamming en Haskell”

LI2011: Deducción natural en lógica proposicional (1)

En la clase de hoy del curso Lógica Informática se ha empezado el estudio de la deducción natural en lógica proposicional.

La reglas que se han visto en la clase son las de la conjunción, de la doble negación, de eliminación del condicional, de modus tollens, de introducción del condicional y las de la disyunción.

También se ha presentado el sistema Pandora para editar demostraciones por deducción natural.

Como tarea pendientes se propone la resolución de los 36 primeros apartados del ejercicio 5 del tema 2 del libro de ejercicios.

Las transparencias de esta clase son las páginas 1-12 del tema 1
Read More “LI2011: Deducción natural en lógica proposicional (1)”