LI2011-12: Sintaxis y semántica de la lógica proposicional

El objetivo fundamental de la clase de hoy del curso Lógica Informática ha consistido en responder estas dos preguntas:

  • ¿cómo se puede construir un programa para que dada una cadena de caracteres decida si es una fórmula proposicional?
  • ¿cómo se puede construir un programa para que dada una fórmula decida si es verdadera?

Para responder a la primera pregunta, desarrollamos la sintaxis de la lógica proposicional. Pero antes de abordar la respuesta, nos planteamos otro análogo que es el reconocimiento de los números naturales. Los números naturales pueden representarse por 0, s(0), s(s(0)), … La pregunta es ¿cómo se puede construir un programa para que dada una cadena de caracteres decida si es un número natural? Una respuesta se basa en utilizar las dos reglas siguientes:

  • 0 es un número natural;
  • si n es un número natural, entonces s(n) es un número natural.

Vemos que es una definición recursiva con un elemento básico (el 0) y un constructor (s, que representa el siguiente). Basado en esta analogía se define las fórmulas proposicionales tomando como elementos básicos las fórmulas atómicas y como constructores las conectivas.

La siguiente cuestión que nos planteamos es cómo definir procedimientos sobre fórmulas. Volvemos a apoyarnos en los números naturales y vemos cómo se puede definir la suma de dos números naturales:

  • 0 + y = y
  • s(n) + y = s(n+y)

Vemos que es una definición por recursión en el primer argumento con dos casos correspondientes a las dos reglas de definición de los números naturales. En el caso de las fórmulas proposicionales las definiciones tendrá una ecuación para las fórmulas atómicas y una por cada una de las conectivas (aunque generalmente las binarias se agrupen en una única ecuación). Como ejemplo de definiciones sobre fórmulas se definen funciones para calcular el número de paréntesis y el conjunto de subfórmulas de una fórmula.

La tercera cuestión sintáctica que nos planteamos es cómo demostrar que todas las fórmulas cumplen una propiedad. De nuevo nos apoyamos en la aritmética y recordando el principio de inducción sobre los números naturales introducimos el principio de inducción sobre fórmulas.

Para responder a la primera pregunta, desarrollamos la semántica de la lógica proposicional. En primer lugar, el valor de verdad de una fórmula en una interpretación se define por recursión. A partir del valor de verdad podemos, dada una fórmula F, dividir las interpretaciones entre las que son modelo de F y las que no lo son. Además, las fórmulas pueden clasificarse en satisfacibles (las que tienen modelos) e insatisfacibles (en caso contrario). Las fórmulas satisfacibles se pueden clasificar en tautologías (para las que todas las interpretaciones son modelo) y contingentes (en caso contrario).

Al final de la clase se han comentado soluciones de ejercicios de formalización con APLI2 que han presentado mayores dificultades en su resolución

Los ejercicios pendientes para la próxima clase son desde el 22 al 26 del capítulo 1 del libro de ejercicios.

Las transparencias de esta clase son las páginas 6-20 del tema 1
Read More “LI2011-12: Sintaxis y semántica de la lógica proposicional”

LI2011-12: Panorama de la lógica. La lógica proposicional como sistema de representación del conocimiento

La clase de hoy del curso Lógica Informática ha tenido dos partes.

En la primera parte se ha presentado un panorama de la Lógica Informática en la que se ha visto su concepto (Lógica Informática = Representación del conocimiento + Automatización del razonamiento), distintas lógicas y aplicaciones de la lógica en Informática.

En la segunda parte se ha presentado la lógica proposicional como sistema de representación del conocimiento. También se ha presentado el sistema APLI2 que sirve de tutor para el aprendizaje de la representación lógica del conocimiento.

Las tareas pendientes son:

  • registrarse en APLI2 y
  • resolver ejercicios de formalización proposicional con APLI2

Las transparencias de esta clase son las páginas 1-5 del tema 1
Read More “LI2011-12: Panorama de la lógica. La lógica proposicional como sistema de representación del conocimiento”

Reseña: Implementation of Bourbaki’s Elements of Mathematics in Coq. Part Two: Ordered Sets, Cardinals, Integers

En una entrada anterior comentamos el proyecto de formalización del libro Elements of Mathematics: Theory of Sets de N. Bourbaki en Coq.

En dicha entrada comentamos el primer paso del proyecto consistente en la formalización de la teoría de conjuntos correspondiente al capítulo II del libro de Bourbaki (páginas 65-130).

La formalización del capítulo III (páginas 131-256) constituye el contenido del segundo paso. Dicha formalización ha sido publicada por José Grimm en el artículo Implementation of Bourbaki’s Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers. Su resumen es el siguiente

We believe that it is possible to put the whole work of Bourbaki into a computer. One of the objectives of the Gaia project concerns homological algebra (theory as well as algorithms); in a first step we want to implement all nine chapters of the book Algebra. But this requires a theory of sets (with axiom of choice, etc.) more powerful than what is provided by Ensembles; we have chosen the work of Carlos Simpson as basis. This reports lists and comments all definitions and theorems of the Chapter Ordered Sets, Cardinals, Integers”.

Version 3 is based on the Coq ssreflect library. It implements some properties on ordinal numbers. The code (including some exercises) is available on the Web, under http://www-sop.inria.fr/apics/gaia.

LI2011-12: Presentación del curso de “Lógica informática” (2011-12)

En la clase de hoy, se ha realizado la presentación del curso Lógica Informática siguiendo el plan de la asignatura. Se ha comentado el contenido de la asignatura, el sistema de evaluación y los materiales de la asignatura en la Red: