Autor Tema: Proof Designer: Esquema de demostraciones en teoría elemental de conjuntos

0 Usuarios y 1 Visitante están viendo este tema.

06 Agosto, 2020, 10:01 am
Leído 310 veces

manooooh

  • Matemático
  • Mensajes: 2,967
  • País: ar
  • Karma: +1/-0
  • Sexo: Masculino
Hola!!

Leyendo un libro que encontré en Internet llamado "How to Prove it" de Daniel J. Velleman (se encuentra en la web), y recordando aquel hilo del foro muy importante para mí: El juego de los números naturales: demostraciones asistidas con Lean, creado por geómetracat, pensé en si había más herramientas que permitiesen probar teoremas matemáticos usando un ordenador. Y la respuesta parece ser sí.

Como Velleman describe en su página académica:

Proof Designer [is] a java applet that writes outlines of proofs in elementary set theory, under the guidance of the user. It is designed to help students learn to write proofs. Proof Designer's approach to proof-writing is similar to the approach used in my book How to Prove it. An old Mac Classic version of Proof Designer is also available.

La página del Proof Designer es: https://app.cs.amherst.edu/~djvelleman/pd/pd.html

Lamentablemente nunca trabajé con applets de Java pero tengo entendido que hay que descargarse un utilitario para manejarlo, aunque dice que también funciona con ciertos navegadores pero la verdad que no supe cómo hacerlo.

Invoco a geómetracat y otros usuarios que quieran sumarse, ¿pueden testear dicha herramienta a ver qué tal? ¿Cómo luce? ¿Cuál es su alcance? Y también pueden dejar su opinión :). Porque no lo pude probar.

Gracias!!
Saludos

06 Agosto, 2020, 03:35 pm
Respuesta #1

geómetracat

  • Moderador Global
  • Mensajes: 1,675
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
Gracias por compartirlo.
Me ha costado bastante, pero al final he conseguido ejecutarlo. Del applet de Java mejor olvidarse, porque parece que la mayoría de navegadores modernos ya no lo soportan (o es muy difícil de habilitar, yo no lo he conseguido). Pero me he bajado la "New Version" que es un archivo Java ejecutable, y éste sí me ha funcionado.

En cuanto al programa en sí, yo diría que tiene bastante poco que ver con Lean y otros parecidos. Éste es un demostrador de teoremas "de juguete", supongo que pensado principalmente para que los lectores del libro practiquen. Las funcionalidades son bastante limitadas (solamente hay disponibles los símbolos típicos de teoría elemental de conjuntos, y no parece que haya posibilidad de crear definiciones). Por otro lado, hay que hacer todas las acciones a través de menús, con lo que no te queda un programa (una lista de instrucciones con la demostración) que puedas enseñar a otras personas. Y además no parece que puedas usar cosas ya probadas, a no ser que las metas explícitamente como hipótesis. En definitiva, que parece un programa pensado para hacer ejercicios muy sencillos de teoría de conjuntos (los típicos problemas de álgebra de Boole de conjuntos), pero no para nada más complicado que eso.

Por cierto, he echado a faltar algún tutorial y algunos ejemplos resueltos, he tenido que estar un rato hasta descubrir cómo hacer algo.

Por otra parte, este programa está basado en lógica de primer orden (las expresiones de conjuntos se reducen a fórmulas lógicas), mientras que programas más serios de demostración automática suelen estar basados en teorías de tipos dependientes.

Esto es todo lo que puedo decir sobre el programa después de haber estado jugando un rato.
La ecuación más bonita de las matemáticas: \( d^2=0 \)

07 Agosto, 2020, 12:21 am
Respuesta #2

manooooh

  • Matemático
  • Mensajes: 2,967
  • País: ar
  • Karma: +1/-0
  • Sexo: Masculino
Hola

Muchas gracias por compartir tu experiencia!! Tienes razón; parece más de juguete que una potente herramienta de demostración.

Hice como dijiste y me bajé el .jar de New Version, y parece que no hace ningún tipo de inferencias.

Por otra parte, este programa está basado en lógica de primer orden (las expresiones de conjuntos se reducen a fórmulas lógicas), mientras que programas más serios de demostración automática suelen estar basados en teorías de tipos dependientes.

Quién lo diría; algo tan común para nosotros no se usa en los ordenadores. ¡Qué interesante!

Saludos