Reseña: Coq, a proof assistant based on higher-order intuitionistic type theory

La semana pasada Jean-Pierre Jouannaud hizo una presentación sobre razonamiento automático en el Instituto de estudios avanzados de la Universidad de Tsinghua: Coq, a proof assistant based on higher-order intuitionistic type theory.

En la presentación se incluyen comentarios sobre objetivos y logros del razonamiento formalizado, los fundamentos teóricos de los demostradores, la correspondencia de Curry-Horward, el cálculo de construcciones de Coq y su adecuación.

LI2011-12: Representación del conocimiento mediante lógica de primer orden

En la clase de hoy del curso Lógica Informática se presentado la lógica de primer orden como sistema de representación del conocimiento.

La clase ha comenzado recordando la ecuación que resumen el curso: LI=RC+AR, donde LI = Lógica informática, RC = Representación del conocimiento y AR = Automatización del razonamiento.

Ya hemos estudiado el sistema básico de representación del conocimiento (la lógica proposicional) y tres sistemas deductivos (deducción natural, tableros semánticos y resolución). Además, hemos usado Prover9 y MACe4 para resolver problemas que se pueden codificar mediante la lógica proposicional, como el de las 4 reinas. Un inconveniente de las codificaciones es la cantidad y el tamaño de las fórmulas resultantes. En la clase vamos a ver dos formas de reducir el tamaño de las codificaciones.

La primera forma es el uso de las conectivas generalizadas con índices. Para verlo hemos comentado la representación y solución con SAToulouse de rompecabezas lógicos.

La segunda forma es el uso de la lógica de primer orden. Este sistema permite representar de forma más compacta conocimiento representable en lógica proposicional y también representar conocimiento que no se puede representar en lógica proposicional.

Como ejemplos de representación hemos visto cómo representar conocimiento geográfico, del mundo de los bloques y conocimiento astronómico. En los distintos ejemplos hemos resaltado los tipos de símbolos lógicos utilizados.

Finalmente, como tutor para la representación del conocimiento, se ha presentado el APLI2 (APLIcación de Ayuda Para Lógica Informática).

Las transparencias de esta clase son las páginas 1 a 10 del tema 6:
Read More “LI2011-12: Representación del conocimiento mediante lógica de primer orden”

I1M2011: Ejercicios de definiciones por recursión y comprensión en Haskell (1)

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones de los ejercicios de la 7ª relaciónen la que se presentan ejercicios con dos definiciones (una por recursión y otra por comprensión) y la comprobación de la equivalencia de las dos definiciones con QuickCheck. Los ejercicios corresponden al tema 5 y al tema 6.

Los ejercicios, y sus soluciones, se muestran a continuación:
Read More “I1M2011: Ejercicios de definiciones por recursión y comprensión en Haskell (1)”

LI2011-12: Aplicaciones de la lógica proposicional con Prover9 y Mace4

En la clase de hoy del curso Lógica Informática hemos visto cómo resolver lógicamente problemas representándolos en la lógica proposicional y usando Prover9/Mace4 para su solución.

Los problemas que se han visto son

  • El problema de los veraces y los mentirosos.
  • El problema de los animales.
  • El problema del coloreado del pentágono.
  • El problema del palomar.
  • El problema de los rectángulos.
  • El problema de las 4 reinas.
  • El problema de Ramsey.

Como tarea pendiente se propone la solución de problemas análogos siguiendo la misma estructura que los anteriores:

  1. Enunciado.
  2. Simbolización.
  3. Representación.
  4. Búsqueda de la prueba (con Prover9) o de modelos (con Mace4).
  5. Conclusión.

Las transparencias utilizadas son las del tema 5b
Read More “LI2011-12: Aplicaciones de la lógica proposicional con Prover9 y Mace4”

Libro de ejercicios resueltos de programación en Haskell (versión del 9 de Noviembre de 2011)

A lo largo del curso iré actualizando un libro de ejercicios resueltos de programación con Haskell con las relaciones de ejercicios del curso de Informática (de 1º del Grado en Matemáticas)

En la versión actual contiene las soluciones de las 6 primeras relaciones que tratan sobre definiciones elementales, definiciones por comprensión y definiciones por recursión.