Trabajo de Lógica Computacional en Enschede (Países Bajos)

PorJosé A. Alonso

El Grupo de métodos formales de la Universidad de Twente ha ofertado 2 plazas para trabajar en Enschede (Países Bajos): PhD and Post Doc position on ERC project Verifcation of Concurrent Data Structures (U. Twente, Netherlands)

El trabajo consistirá en la especificación y verificación de estructuras de datos concurrentes.

Las dos plazas se incriben en el proyecto VerCors (Verification of Concurrent Data Structures) dirigido por Marieke Huisman.

I1M2010: Definiciones por recursión sobre números naturales y listas

PorJosé A. Alonso

Los objetivos de la clase de hoy son:

  • Aprender a desarrollar aplicaciones usando listas de comprensión. Para ello, se ha desarrollado un programa para descifrar mensajes que usen el cifrado de César.
  • Aprender a definir funciones por recursión sobre los números naturales.
  • Aprender a definir funciones por recursión sobre listas.
  • Aprender a definir funciones por recursión sobre listas que necesiten guardas en el caso recursivo.

Como tarea para la próxima clase se ha propuesto escribir de manera colaborativa las soluciones de los ejercicios de la 5ª relación y de la 6ª relación.

Las transparencias usadas en la clase son las comprendidas entre las páginas 27 y 34 del tema 5 y las 12 primeras del tema 6

Descargar (PDF, 231KB)

I1M2010: Definiciones por comprensión

PorJosé A. Alonso

El objetivo de la clase de hoy es continuar aprendiendo a definir funciones en Haskell usando listas de comprensión. En concreto, se ha visto cómo usar las definiciones por comprensión con las funciones de emparejamiento (zip) y con las cadenas y se ha comenzado como caso de estudio la codificación de César.

Como tarea para la próxima clase se ha propuesto escribir de manera colaborativa las soluciones de los ejercicios de la 5ª relación y de la 6ª relación.

Las transparencias usadas en la clase son las comprendidas entre las páginas 12 y 27 del tema 5

Descargar (PDF, 287KB)

Lectura e introspección

PorJosé A. Alonso

Leyendo el libro de Marvin Minsky ‘La máquina de las emociones (Sentido común, inteligencia artificial y el futuro de la mente humana)” me he encontrado en la página 19 con la siguiente cita de Marcel Proust

Todo lector lee únicamente lo que ya tiene dentro de sí mismo. Un libro no es más que una especie de instrumento óptico que el autor ofrece para dejar que el lector pueda descubrir en sí mismo lo que nunca habría encontrado sin ayuda del libro.

Con esta cita comienzo una nueva sección de Vestigium en la que iré recopilando citas de mis lecturas.

RA2010: Visión panorámica del razonamiento automático

PorJosé A. Alonso

Hoy ha comenzado el curso de Razonamiento automático del Máster Universitario en Lógica, Computación e Inteligencia Artificial de la Universidad de Sevilla.

En la clase de hoy se ha presentado la asignatura y se ha comentado una visión panorámica del razonamiento automático a través de ejemplos con los sistemas de razonamiento Otter/Mace, ACL2, PVS e Isabelle/HOL.
Read More “RA2010: Visión panorámica del razonamiento automático”