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)”

El problema de las puertas en Haskell

En Gaussianos han comentado esta semana El problema de las 100 puertas y los divisores de un número natural cuyo enunciado es el siguiente

Supongamos que tenemos n puertas numeradas del 1 al n que están todas cerradas. Realizaremos, para cada puerta, el siguiente proceso: cambiar de estado todas las puertas cuyo número sea múltiplo de la puerta en la que estemos en ese momento. El problema consiste en caracterizar las puertas que quedan abierta al final del proceso.

Por ejemplo, supongamos que n=5 y usamos A para indicar que la puerta está abierta y C para indicar que está cerrada.

  • Inicialmente, nos encontramos en la posición 1 y el estado de las puertas es CCCCC.
  • Cambiamos de estado todas las puertas que tienen como número un múltiplo de 1 (es decir, en este caso las abrimos todas, con lo que tenemos AAAAA) y aumentamos la posición a 2.
  • Cambiamos de estado todas las puertas que tienen como número un múltiplo de 2, (es decir, cerramos la 2 y la 4, con lo que tenemos ACACA) y aumentamos la posición a 3.
  • Cambiamos de estado todas las puertas que tienen como número un múltiplo de 3, (es decir, cerramos la 3, con lo que tenemos ACCCA) y aumentamos la posición a 4.
  • Cambiamos de estado todas las puertas que tienen como número un múltiplo de 4, (es decir, abrimos la 4, con lo que tenemos ACCAA) y aumentamos la posición a 5.
  • Cambiamos de estado todas las puertas que tienen como número un múltiplo de 4, (es decir, cerramos la 5, con lo que tenemos ACCAC).

En este ejemplo han quedado abiertas la puerta 1 y la puerta 4.

Basándome en este problema he escrito la siguiente relación de ejercicios de Haskell para la asignatura de Informática de 1º del Grado en Matemáticas
Read More “El problema de las puertas en Haskell”

Razonamiento formalizado para la enseñanza de las matemáticas

Un posible campo de aplicación del razonamiento formalizado podría ser su uso como alumno inteligente de forma que “enseñar” al sistema sería una manera de aprender a enseñar, haciendo explícito gran parte del conocimiento implícito.

Parece que una idea parecida pudo tener N.G. de Bruijn (el autor de Automath, el primer sistema de razonamiento formalizado) al afirmar que

If you can’t explain your mathematics to a machine it is an illusion to think you can explain it to a student.