LI2011-12: Ejercicios de lógica de primer orden

La clase de hoy del curso Lógica Informática ha consistido en la resolución de ejercicios de la lógica de primer orden. Los ejercicios corresponden al capítulo 6 del libro de ejercicios, aunque en su solución se han utilizado tableros semánticos.

Los ejercicios resueltos son los siguientes:

  • Decidir la consistencia de conjuntos de fórmulas mediante tableros semánticos infinitos (por ejemplo, del conjunto \{N(0), \forall x (N(x) \to N(s(x))\}.
  • Determinar las variables libres y las ligadas de una fórmula (ejercicio 6.28).
  • Decidir la satisfacibilidad de fórmulas con variables libres (ejercicio 6.29.1).
  • Decidir la validez de fórmulas con variables libres (ejercicio 6.29.3).
  • Decidir la validez de una fórmula en una estructura dada (ejercicio 6.30).
  • Decidir la consistencia de un conjunto de fórmulas (ejercicio 6.31).
  • Decidir si una fórmula es consecuencia de un conjunto de fórmulas (ejercicio 6.32).

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

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

En la primera parte, se ha comentado formalizaciones de argumentos en la lógica de primer orden usando APLI2. En concreto, los ejercicios 2, 3, 7, 8, 9 y 12. También hemos visto una forma de facilitar la corrección de los errores sintácticos: escribir la fórmula en Prover9 y preguntarle si está bien escrita.

En la segunda parte, se ha presentado la ampliación del cálculo de deducción natural proposional para tratar los cuantificadores y las igualdades.

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

Las transparencias de esta clase son las del tema 7 que se muestran a continuación
Read More “LI2011-12: Deducción natural en lógica de primer orden”

I1M2011: Patrones de plegado en Haskell

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado cómo puede abstraerse los esquemas definición de funciones de recursión sobre listas mediante la función de plegado (foldr) y cómo con dicha función puede simplificarse la definición de funciones.

A continuación se ha visto cómo definir funciones con acumuladores y cómo simplificarlas con el patrón de plegado por la izquierda (foldl).

Finalmente, se ha visto cómo puede simplificarse la definición de funciones usando el operador de composición.

Las transparencias usadas en la clase son las páginas 12 a 22 del tema 7
Read More “I1M2011: Patrones de plegado en Haskell”

RA2011: Semántica de la lógica de primer orden

En la clase de hoy del curso de Razonamiento automático se ha presentado la semántica de la lógica de primer orden.

Hemos empezado viendo ejemplos para ver de qué depende la verdad de una fórmula: del universo, de la interpretación de los símbolos constantes y de la asignación a las variables libres.

A partir de estos ejemplos, se introduce los conceptos de

  • estructura {\cal I} (formadas por un universo U junto con la interpretación I de las constantes, funciones y relaciones),
  • asignación a las variables en una estructura (A) e
  • interpretación (formada por una estructura junto con una asignación)

A continuación, se definen los siguientes conceptos:

  • valor de un término en una interpretación ({\cal I}_A(t)),
  • valor de ua fórmula en una interpretación ({\cal I}_A(F)),
  • realización de una fórmula ({\cal I}_A \models F),
  • satisfacibilidad de una fórmula en una interpretación,
  • validez de una fórmula en una estructura ({\cal I} \models F),
  • modelo de una fórmula ({\cal I} \models F),
  • satisfacibilidad de una fórmula,
  • validez de una fórmula (\models F),
  • realización de un conjunto de fórmulas ({\cal I}_A \models S),
  • consistencia de un conjunto de fórmulas,
  • modelo de un conjunto de fórmulas ({\cal I} \models S),
  • consecuencia lógica (S \models F),
  • equivalencia lógica (F \equiv G),

También se ha estudiados las relaciones entre los anteriores conceptos.

Las transparencias de la clase son las páginas 23 a 51 del tema 1.