DAO2011: Isabelle como un lenguaje funcional

PorJosé A. Alonso

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

PorJosé A. Alonso

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)

PorJosé A. Alonso

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)”

LI2011: Semántica de la lógica proposicional (2)

PorJosé A. Alonso

En la clase de hoy del curso Lógica Informática se ha completado el estudio de la semántica proposicional desde el punto de vista computacional; es decir, se ha ido definidendo los conceptos semánticos y comentando su posible implementación.

Los conceptos definidos son equivalencia de fórmulas, modelos de conjuntos de fórmulas, conjuntos consistentes e inconsistentes y consecuencia lógica.

Se ha demostrado la equivalencia de los siguientes problemas

  1. decidir si una fórmula es consecuencia lógica de un conjunto finito de fórmulas,
  2. decidir si una fórmula es una tautología,
  3. decidir si una fórmula es insatisfacible y
  4. decidir si un conjunto de fórmulas es inconsistente.

Como aplicación se ha visto la decisión de la corrección de un argumento y la resolución de rompecabezas lógicos. En la solución del rompecabeza se ha explicado el uso del Gateway to Logic.

Se ha comentado las soluciones de los ejercicios 25, 32 y 33 del tema 1.

Como tarea pendientes se propone la resolución de los restantes ejercicios del tema 1 del libro de ejercicios.

Las transparencias de esta clase son las páginas 26-34 del tema 1
Read More “LI2011: Semántica de la lógica proposicional (2)”