Demostrar el teorema de Nicómaco que afirma que la suma de los cubos de los \(n\) primeros números naturales es igual que el cuadrado de la suma de los \(n\) primeros números naturales; es decir, para todo número natural n se tiene que \[ 1^3 + 2^3 + ... + n^3 = (1 + 2 + ... + n)^2 \]
El problema de hoy está basado en el reto Daily Challenge #168 que se planteó ayer. El reto consiste en demostrar que si f es una función de los booleanos en los booleanos, entonces para todo b se verifica que f (f (f b)) = f b.
Concretamente, el reto consiste en completar la siguiente demostración
lemma fixes f :: "bool ⇒ bool" shows "f (f (f b)) = f b" sorry
Decidir si es cierto que
"Existe una Universidad tal que si en dicha Universidad se celebra el Día Mundial de la Lógica (DML), entonces en todas las Universidades se celebra el DML."
En la formalización usar C(x) para representar que en la Universidad x se celebra el DML.
El Consejo Ejecutivo de la UNESCO ha proclamado el 14 de enero como Día mundial de la jógica.
La fecha del 14 de enero se ha eligido para rendir homenaje a dos grandes lógicos del siglo XX: Kurt Gödel (que falleció el 14 de enero de 1978) y Alfred Tarski (que nació el 14 de enero de 1901).
Uniéndose a dicha celebración, hoy (14 de enero de 2020) comienza la andadura de este blog cuyo principal objetivo es servir de complemento a las asignaturas de
El plan es proponer cada semana un ejercicio de forma que los alumnos pueden escribir las soluciones en los comentarios utilizando Isabelle/HOL en la demostración.
El código se escribe entre una línea con <pre lang="isar"> y otra con </pre>