Wolfram Alpha, ese poco conocido "motor de conocimiento" con aspecto de buscador que cuenta con gigantescas bases de datos estructuradas y con el cerebro de Mathematica, permite generar pruebas matemáticas mediante inducción a partir de una consulta en lenguaje normal y corriente. Un ejemplo típico sería: "Demostrar que 8 elevado a n menos 3 elevado a n es divisible por 5 para cualquier valor de n mayor que 0."
No hace tiempo que existen demostradores automáticos que hacen eso...
como siempre los de microsiervos se lucen en los titulares. Lo que es nuevo es elegir demostración por inducción a partir de una pregunta en lenguaje natural.
Comentarios
No hace tiempo que existen demostradores automáticos que hacen eso...
como siempre los de microsiervos se lucen en los titulares. Lo que es nuevo es elegir demostración por inducción a partir de una pregunta en lenguaje natural.
Ahora solo les falta alguien que las entienda.
¡Abajo la inducción! ¡Viva la deducción!