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

La clase de hoy del curso Lógica matemática y fundamentos ha tenido tres partes.

En la primera parte se ha presentado un panorama de la lógica en la que se ha visto sus objetivos (representar el conocimiento y automatizar el razonamiento), distintas lógicas (proposicional, primer orden, orden superior y modales) y aplicaciones de la lógica en computación.

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.

En la tercera parte se ha iniciado el estudio de la sintaxis de la lógica proposicional mostrando cómo se definen las fórmulas por recursión, cómo se definen funciones sobre las fórmulas mediante recursión y cómo se demuestran propiedades de las fórmulas mediante inducción.

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-10 del tema 1
Read More “LMF2012: Panorama de la lógica. La lógica proposicional como sistema de representación del conocimiento”

I1M2011: Ejercicios con definiciones por recursión y comprensión en Haskell (3)

La clase de hoy de Informática de 1º del Grado en Matemáticas hemos terminado continuado comentando soluciones de ejercicios con definiciones por recursión y comprensión. Concretamente, hemos visto los la 7ª relación (que comenzamos en la clase del día 22 y continuamos en la clase del 25) y los de la 8ª relación.

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

I1M2011: Ejercicios de definiciones por recursión en Haskell (2)

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos continuado los comentarios sobre las soluciones de los ejercicios de la 6ª relación, que tratan sobre definiciones por recursión, que comenzamos en la clase anterior.

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

Lecturas de razonamiento formalizado (del 27-Oct-2010 al 1-Jul-2011)

Esta entrada es una recopilación de lecturas sobre razonamiento formalizado que hemos compartido este curso en la lista de correo del grupo de lógica computacional.

La recopilación de los está ordenada según el sistema de razonamiento utilizado (ACL2, Agda, Coq, HOL, Isabelle, Matita, Mizar, Otter/Prover9, PVS ó Twelfe) y, dentro de cada uno, por la fecha de su publicación.

Read More “Lecturas de razonamiento formalizado (del 27-Oct-2010 al 1-Jul-2011)”