LI2011-12: Resolución en lógica de primer orden

En la clase de hoy del curso Lógica Informática se ha presentado la resolución en la lógica de primer orden como ampliación del presentado en el tema 5 para la lógica proposicional.

Las principales diferencias se encuentran en la unificación, separación de variables y factorización.

Además, se ha presentado el sistema Prover9 que busca automáticamente demostraciones por resolución.

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

Las transparencias de esta clase son las del tema 11
Read More “LI2011-12: Resolución en lógica de primer orden”

LI2011-12: Modelos de Herbrand

En la clase de hoy del curso Lógica Informática se estudiado cómo se puede puede reducir la consistencia de conjuntos de cláusulas de primer orden a la consistencia de conjuntos de cláusulas proposicionales.

En primer lugar, se ha observado que la reducción es inmediata en el caso de fórmulas sin variables.

A continuación se han presentado procedimientos para construir los universos de Herbrand, las bases de Herbrand y las interpretaciones de Herbrand. Así como un procedimiento que transforma modelos de conjuntos de cláusulas en modelos de Herbrand. Por tanto, la consistencia de un conjunto de cláusulas se reduce a la búsqueda de modelos de Herbrand.

Finalmente, se ha explicado el teorema de Herbrand y su aplicación para decidir la consistencia de un conjunto de cláusulas buscando un subconjunto finito de su extensión de Herbrand que sea consistente (en el sentido proposicional).

Las transparencias de la clase son las tema 10.

Libro de ejercicios resueltos de programación en Haskell (versión del 19 de Diciembre 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 9 primeras relaciones y los 2 primeros exámenes:

  1. Definiciones elementales de funciones (1).
  2. Definiciones elementales de funciones (2).
  3. Definiciones por comprensión (1).
  4. Definiciones por comprensión (2).
  5. Definiciones por comprensión (3): El cifrado César.
  6. Definiciones por recursión.
  7. Definiciones por recursión y por comprensión (1).
  8. Definiciones por recursión y por comprensión (2).
  9. Definiciones sobre cadenas, orden superior y plegado.
  10. Exámenes:
    • Examen 1 (26 de Octubre de 2011).
    • Examen 2 (30 de Noviembre de 2011).

El libro se ha ampliado en la versión del 8 de Febrero de 2012.