RA2010: Panorama del razonamiento automático con Isabelle/HOL

PorJosé A. Alonso

La clase de hoy es la última del curso de Razonamiento automático. Se ha hecho una presentación de distintas aplicaciones que ayudan en el desarrollo de formalización del razonamiento con Isabelle/HOL y pequeños casos de estudi. Concretamente,

El código correspondiente se encuentra en Tema8.thy .

LI2011: La lógica proposicional como sistema de representación del conocimiento y su sintaxis

PorJosé A. Alonso

En la clase de hoy del curso Lógica Informática ha tenido tres 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.

En la tercera parte se ha presentado la sintaxis de la lógica proposicional. Concretamente,

  • el lenguaje de la lógica proposicional,
  • la definición recursiva de las fórmulas proposicionales,
  • árboles de análisis de fórmulas,
  • definiciones por recursión sobre fórmulas y
  • demostraciones por inducción sobre fórmulas.

Las tareas pendientes son:

  • registrarse en APLI2,
  • resolver ejercicios de formalización proposicional con APLI2 y
  • resolver los ejercicios 22, 23, 24 y 25 del capítulo 1 del libro de ejercicios.

Las transparencias de esta clase son las páginas 1-13 del tema 1
Read More “LI2011: La lógica proposicional como sistema de representación del conocimiento y su sintaxis”

I1M2010: Problema del concurso “Cifras y letras” en Haskell

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comenzado a desarrollar un programa en Haskell para resolver los problemas aritméticos del concurso Cifras y letras que consisten en dada una sucesión de números naturales y un número objetivo, intentar construir una expresión cuyo valor es el objetivo combinando los números de la sucesión usando suma, resta, multiplicación, división y paréntesis. Además, cada número de la sucesión puede usarse como máximo una vez y todos los números, incluyendo los resultados intermedios tienen que ser enteros positivos (1,2,3,…).

Por ejemplo, dada la sucesión 1, 3, 7, 10, 25, 50 y el objetivo 765, una solución es (1+50)*(25−10). Para el problema anterior existen 780 soluciones. En cambio, con la sucesión anterior y el objetivo 831, no hay solución.

Las transparencias usadas en la clase son las página 1 a 12 del tema 11:
Read More “I1M2010: Problema del concurso “Cifras y letras” en Haskell”

I1M2010: Razonamiento sobre programas Haskell

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado cómo demostrar propiedades de funciones definidas en Haskell. Los esquemas de demostración estudiados son:

  • por simplificación,
  • por casos,
  • por inducción sobre los números naturales,
  • por inducción sobre listas,
  • por inducción anidada y
  • por generalización e inducción.

Las transparencias usadas en la clase son las del tema 8:
Read More “I1M2010: Razonamiento sobre programas Haskell”