I1M2013: Definiciones por composición de funciones aritméticas

PorJosé A. Alonso

En la clase de hoy del curso Informática (de 1º del Grado en Matemáticas) se han resuelto los ejercicios de la 1ª relación. El objetivo de dicha relación es habituar a los alumnos con el entorno de trabajo Haskell/Emacs resolviendo ejercicios con definiciones de funciones por composición de las primitivas de Haskell sobre aritmética.

Los ejercicios y sus soluciones se muestran a continuación
Read More “I1M2013: Definiciones por composición de funciones aritméticas”

LI2013: Sintaxis de la lógica proposicional

PorJosé A. Alonso

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

En la primera parte se ha comentado las soluciones de la 1ª relación de ejercicios de representación del conocimiento en lógica proposicional usando Isabelle/HOL.

En la segunda parte se ha presentado un panorama de la lógica y sus aplicaciones a la informática. Como ejemplo de aplicación se ha mostrado cómo se puede generar automáticamente programas usando MagicHaskeller.

En la tercera parte se ha explicado la sintaxis de la lógica proposicional insistiendo en el carácter inductivo del tipo de datos de las fórmulas proposicionales, del procedimiento de definiciones por recursión sobre las fórmulas y de demostración de propiedades por inducción sobre las fórmulas.

Las tareas propuestas son:

  • resolver los ejercicios de la 2ª relación de representación del conocimiento proposicional en Isabelle/HOL y
  • resolver los ejercicios 22 a 24 del tema 2 (páginas 11 y 12 del libro de ejercicios).

Las transparencias de esta clase son las páginas 2-13 del tema 1
Read More “LI2013: Sintaxis de la lógica proposicional”

A fully automatic problem solver with human-style output

PorJosé A. Alonso

Se ha publicado un artículo sobre automatización del razonamiento titulado A fully automatic problem solver with human-style output.

Sus autores son Mohan Ganesalingam y Timothy Gowers.

Su resumen es

This paper describes a program that solves elementary mathematical problems, mostly in metric space theory, and presents solutions that are hard to distinguish from solutions that might be written by human mathematicians. The program is part of a more general project, which we also discuss.

LI2013: Presentación del curso de “Lógica informática”

PorJosé A. Alonso

En la primera parte de la clase de hoy, se ha presentado el 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:

En la segunda parte, se ha explicado la instalación y uso de Isabelle/HOL. Como ejemplo se ha resuelto el primer ejercicio de la 1ª relación. Finalmente se ha explicado cómo publicar la solución en la wiki.

Como tarea para la próxima clase, se ha propuesto la solución de los ejercicios de la 1ª relación.

I1M2013: Introducción a la programación con Haskell

PorJosé A. Alonso

En la segunda parte de la clase de hoy del curso Informática (de 1º de Grado en Matemáticas) se ha presentado una introducción a la programación con Haskell usando emacs como entorno de programación. Concretamente, se ha explicado cómo

  • usar Haskell como calculadora aritmética (con las funciones +, -, *, /, div y ^).
  • escribir guiones de Haskell en emacs.
  • cargar los guiones y evaluar expresiones con las funciones definidas.

Como tarea para la próxima clase se ha propuesto instalar GHC y emacs (cuyos enlaces se encuentran en la página de sistemas y escribir de manera colaborativa las soluciones de los ejercicios de la 1º relación y de la 2º relación.

Las sesiones se encuentran grabadas en dos vídeos:

  • en el primer vídeo se muestra cómo trabajar con guiones en Haskell dentro de emacs,
  • en el segundo vídeo se muestra cómo trabajar con las relaciones de ejercicios y la wiki.

Las transparencias usadas en la clase son las del tema 2:
Read More “I1M2013: Introducción a la programación con Haskell”