Contenido de Vestigium

Los 400 últimos artículos de Vestigium son

• La semana en Calculemus (25 de mayo de 2024)
• La semana en Calculemus (18 de mayo de 2024)
• La semana en Calculemus (11 de mayo de 2024)
• La semana en Calculemus (4 de mayo de 2024)
• Resumen de lecturas compartidas durante abril de 2024
• El mes de abril en Exercitium (Ejercicios con Haskell y Python)
• La semana en Calculemus (27 de abril de 2024)
• La semana en Calculemus (21 de abril de 2024)
• El mes de marzo en Exercitium (Ejercicios con Haskell y Python)
• La semana en Calculemus (16 de marzo de 2024)
• La semana en Calculemus (9 de marzo de 2024)
• La semana en Calculemus (2 de marzo de 2024)
• La semana en Calculemus (24 de febrero de 2024)
• La semana en Calculemus (3 de febrero de 2024)
• La semana en Calculemus (27 de enero de 2024)
• La semana en Calculemus (20 de enero de 2024)
• La semana en Calculemus (13 de enero de 2024)
• La semana en Calculemus (6 de enero de 2024)
• La semana en Calculemus (30 de diciembre de 2023)
• La semana en Calculemus (10 de diciembre de 2023)
• La semana en Calculemus (2 de diciembre de 2023)
• La semana en Calculemus (25 de noviembre de 2023)
• La semana en Calculemus (18 de noviembre de 2023)
• La semana en Calculemus (11 de noviembre de 2023)
• La semana en Calculemus (5 de noviembre de 2023)
• El mes de octubre en Exercitium (Ejercicios con Haskell y Python)
• La semana en Calculemus (28 de octubre de 2023)
• La semana en Calculemus (21 de octubre de 2023)
• La semana en Calculemus (14 de octubre de 2023)
• La semana en Calculemus (7 de octubre de 2023)
• El mes de septiembre en Exercitium (Ejercicios con Haskell y Python)
• La semana en Calculemus (30 de septiembre de 2023)
• La semana en Calculemus (23 de septiembre de 2023)
• La semana en Calculemus (16 de septiembre de 2023)
• La semana en Calculemus (9 de septiembre de 2023)
• El mes en Exercitium (Ejercicios con Haskell y Python, septiembre de 2023)
• La semana en Calculemus (2 de septiembre de 2023)
• La semana en Calculemus (26 de agosto de 2023)
• La semana en Calculemus (19 de agosto de 2023)
• La semana en Calculemus (12 de agosto de 2023)
• La semana en Calculemus (5 de agosto de 2023)
• La semana en Calculemus (29 de julio de 2023)
• La semana en Calculemus (22 de julio de 2023)
• La semana en Calculemus (15 de julio de 2023)
• La semana en Exercitium (8 de julio de 2023)
• La semana en Exercitium (1 de julio de 2023)
• La semana en Exercitium (24 de junio de 2023)
• La semana en Exercitium (17 de junio de 2023)
• La semana en Exercitium (10 de junio de 2023)
• La semana en Exercitium (3 de junio de 2023)
• La semana en Exercitium (27 de mayo de 2023)
• La semana en Exercitium (20 de mayo de 2023)
• La semana en Exercitium (13 de mayo de 2023)
• La semana en Exercitium (6 de mayo de 2023)
• La semana en Exercitium (29 de abril de 2023)
• La semana en Exercitium (22 de abril de 2023)
• La semana en Exercitium (15 de abril de 2023)
• La IA y la infinitud de números pares que terminan en 7
• La semana en Exercitium (1 de abril de 2023)
• La semana en Exercitium (25 de marzo de 2023)
• La semana en Exercitium (18 de marzo de 2023)
• La semana en Exercitium (11 de marzo de 2023)
• La semana en Exercitium (4 de marzo de 2023)
• Prácticas sobre tipos algebraicos de datos en Haskell con ChatGPT
• ChatGPT como profesor de historia de las matemáticas
• ChatGPT como profesor de programación con Haskell
• La semana en Exercitium (25 de febrero de 2023)
• La semana en Exercitium (18 de febrero de 2023)
• PFH: La semana en Exercitium (11 de febrero de 2023)
• Relaciones entre la programación funcional y las matemáticas, según ChatGPT
• PFH: La semana en Exercitium (4 de febrero de 2023)
• PFH: La semana en Exercitium (28 de enero de 2023)
• PFH: La semana en Exercitium (21 de enero de 2023)
• PFH: La semana en Exercitium (14 de enero de 2023)
• PFH: La semana en Exercitium (7 de enero de 2023)
• PFH: La semana en Exercitium (31 de diciembre de 2022)
• PFH: La semana en Exercitium (24 de diciembre de 2022)
• PFH: La semana en Exercitium (17 de diciembre de 2022)
• PFH: La semana en Exercitium (10 de diciembre de 2022)
• Errores matemáticos en las respuestas de ChatGPT
• DAO: La semana en Calculemus (4 de diciembre de 2022)
• PFH: La semana en Exercitium (3 de diciembre de 2022)
• DAO: La semana en Calculemus (27 de noviembre de 2022)
• PFH: La semana en Exercitium (26 de noviembre de 2022)
• DAO: La semana en Calculemus (18 de noviembre de 2022)
• PFH: La semana en Exercitium (18 de noviembre de 2022)
• DAO: La semana en Calculemus (11 de noviembre de 2022)
• PFH: La semana en Exercitium (11 de noviembre de 2022)
• DAO: La semana en Calculemus (4 de noviembre de 2022)
• PFH: La semana en Exercitium (4 de noviembre de 2022)
• DAO: La semana en Calculemus (28 de octubre de 2022)
• PFH: La semana en Exercitium (28 de octubre de 2022)
• DAO: La semana en Calculemus (21 de octubre de 2022)
• PFH: La semana en Exercitium (21 de octubre de 2022)
• PFH: La semana en Exercitium (14 de octubre de 2022)
• PFH: La semana en Exercitium (7 de octubre de 2022)
• DAO: La semana en Calculemus (30 de septiembre de 2022)
• PFH: La semana en Exercitium (30 de septiembre de 2022)
• DAO: La semana en Calculemus (23 de septiembre de 2022)
• PFH: La semana en Exercitium (23 de septiembre de 2022)
• DAO: La semana en Calculemus (16 de septiembre de 2022)
• PFH: La semana en Exercitium (16 de septiembre de 2022)
• DAO: La semana en Calculemus (9 de septiembre de 2022)
• PFH: La semana en Exercitium (9 de septiembre de 2022)
• DAO: La semana en Calculemus (2 de septiembre de 2022)
• PFH: La semana en Exercitium (2 de septiembre de 2022)
• DAO: La semana en Calculemus (28 de agosto de 2022)
• PFH: La semana en Exercitium (26 de agosto de 2022)
• PFH: La semana en Exercitium (19 de agosto de 2022)
• PFH: La semana en Exercitium (12 de agosto de 2022)
• PFH: La semana en Exercitium (5 de agosto de 2022)
• PFH: La semana en Exercitium (29 de julio de 2022)
• PFH: La semana en Exercitium (22 de julio de 2022)
• PFH: La semana en Exercitium (15 de julio de 2022)
• PFH: La semana en Exercitium (9 de julio de 2022)
• PFH: La semana en Exercitium (1 de julio de 2022)
• PFH: La semana en Exercitium (25 de junio de 2022)
• PFH: La semana en Exercitium (11 de junio de 2022)
• PFH: La semana en Exercitium (del 30 de mayo al 3 de junio de 2022)
• PFH: La semana en Exercitium (del 23 al 27 de mayo de 2022)
• PFH: La semana en Exercitium (del 16 al 20 de mayo de 2022)
• PFH: La semana en Exercitium (del 9 al 13 de mayo de 2022)
• DAO: La semana en Calculemus (del 2 al 6 de mayo de 2022)
• PFH: La semana en Exercitium (del 2 al 6 de mayo de 2022)
• DAO: La semana en Calculemus (del 25 al 30 de abril)
• PFH: La semana en Exercitium (del 25 al 30 de abril)
• DAO: La semana en Calculemus (del 18 al 23 de abril)
• La semana en Exercitium (del 18 al 23 de abril)
• PFH: La semana en Exercitium (del 11 al 15 de abril)
• La semana en Exercitium (del 4 al 8 de abril)
• PFH: Ejercicios con acciones IO (entrada/salida)
• La semana en Exercitium (del 28 de marzo al 1 de abril)
• La semana en Exercitium (del 21 al 25 de marzo)
• La semana en Exercitium (del 14 al 18 de marzo)
• La semana en Exercitium (del 7 al 11 de marzo)
• PFH: Ejercicios sobre árboles binarios de búsqueda
• PFH: Ejercicios de definiciones por plegado
• PFH: Ejercicios sobre transacciones en Haskell
• PFH: Ejercicios sobre tablas y diccionarios en Haskell
• La semana en Exercitium (del 28 de febrero al 4 de marzo)
• PFH: Tipos de datos algebraicos en Haskell
• PFH: Cadenas de bloques en Haskell
• Reseña: Computational logic: its origins and applications
• Reseña: Windmills of the minds: an algorithm for Fermat’s two squares theorem
• Reseña: Formalizing ordinal partition relations using Isabelle/HOL
• Reseña: A machine-checked direct proof of the Steiner-Lehmus theorem
• Reseña: Completeness theorems for first-order logic analysed in constructive type theory
• Reseña: Formalising Lie algebras in Lean
• Reseña: Why formalize mathematics?
• Reseña: What is the point of computers? A question for pure mathematicians
• Materiales para el estudio de la programación funcional con Haskell
• Resumen de lecturas compartidas durante agosto de 2021
• Resumen de lecturas compartidas durante julio de 2021
• Resumen de lecturas compartidas durante junio de 2021
• Resumen de lecturas compartidas durante mayo de 2021
• Resumen de lecturas compartidas durante abril de 2021
• Resumen de lecturas compartidas durante marzo de 2021
• Resumen de lecturas compartidas durante febrero de 2021
• Resumen de lecturas compartidas durante enero de 2021
• Pruebas en Lean de “La función identidad no está acotada superiormente”
• Negación del universal en Lean: Caracterización de funciones no pares
• Negación del existencial en Lean: Caracterización de números no pares
• Pruebas en Lean de la ley de De Morgan: ¬(P ∧ Q) ↔ ¬P ∨ ¬Q
• Pruebas en Lean de “Un número es par si, y sólo si, lo es su cuadrado”
• Pruebas en Lean de “La relación menor es irreflexiva en los reales”
• Pruebas en Lean de “Si u es una sucesión de Cauchy y a es un punto de acumulación de u, entonces a es el límite de u”
• Pruebas en Lean de “Toda sucesión convergente es una sucesión de Cauchy”
• ForMatUS: Pruebas en Lean de “El punto de acumulación de las convergentes es su límite”
• ForMatUS: Pruebas en Lean de “Las subsucesiones tienen el mismo límite que la sucesión”
• ForMatUS: Pruebas en Lean de “Hay infinitos términos arbitrariamente próximos a los puntos de acumulación”
• ForMatUS: Pruebas en Lean de “Las funciones de extracción no están acotadas”
• ForMatUS: Pruebas en Lean de “La función identidad es menor o igual que la función de extracción”
• ForMatUS: Pruebas en Lean de “Los supremos de las sucesiones no decrecientes son sus límites”
• ForMatUS: Pruebas en Lean de la unicidad del límite de las sucesiones
• Pruebas en Lean de “Si |x – y| ≤ ε, para todo ε > 0, entonces x = y”
• ForMatUS: Si |x| < ε, para todo ε > 0, entonces x = 0
• ForMatUS: Pruebas en Lean del teorema del emparedado
• Resumen de lecturas compartidas durante diciembre de 2020
• Resumen de lecturas compartidas durante noviembre de 2020
• ForMatUS: Pruebas en Lean de propiedades de la composición de funciones (elemento neutro y asociatividad)
• ForMatUS: Pruebas en Lean de que la identidad es biyectiva
• ForMatUS: Pruebas en Lean de que las relaciones reflexivas y euclídeas son de equivalencia
• ForMatUS: Pruebas en Lean de que las equivalencias son los preórdenes simétricos
• Resumen de lecturas compartidas durante octubre de 2020
• ForMatUS: Pruebas en Lean de una desigualdad entre números naturales
• ForMatUS: Pruebas en Lean de que las partes simétricas son simétricas
• ForMatUS: Pruebas en Lean de que las partes simétricas de las relaciones reflexivas son reflexivas
• ForMatUS: Pruebas en Lean de que las partes estrictas de los órdenes parciales son transitivas
• ForMatUS: Pruebas en Lean de que las partes estrictas son irreflexivas
• ForMatUS: Pruebas en Lean de que las relaciones irreflexivas y transitivas son asimétricas
• ForMatUS: Pruebas en Lean de 𝒫 A ⊆ 𝒫 B ↔ A ⊆ B
• ForMatUS: Pruebas en Lean de (⋃i, ⋂j, A i j) ⊆ (⋂j, ⋃i, A i j)
• ForMatUS: Pruebas en Lean de la intersección sobre unión general: C ∩ (⋃i, A i) = (⋃ i, C ∩ A i)
• ForMatUS: Pruebas en Lean de la distributiva de la intersección general sobre la intersección
• ForMatUS: Pertenencia a uniones e intersecciones de familias en Lean
• ForMatUS: Unión e intersección de familias de conjuntos en Lean
• ForMatUS: Pruebas en Lean de (A ∩ Bᶜ) ∪ B = A ∪ B
• PFH: Sistema de decisión de tautologías en Haskell
• ForMatUS: Pruebas en Lean de la propiedad distributiva de la intersección sobre la unión
• ForMatUS: Pruebas en Lean de la conmutatividad de la intersección
• ForMatUS: Complementario de un conjunto en Lean (Pruebas de A \ B ⊆ Bᶜ)
• ForMatUS: Diferencia de conjuntos en Lean (Pruebas de A \ B ⊆ A)
• ForMatUS: Regla del conjunto vacío en Lean
• ForMatUS: Regla de introducción de la unión en Lean
• ForMatUS: Regla de introducción de la intersección en Lean
• ForMatUS: Pruebas en Lean de la antisimetría de la inclusión de conjuntos
• ForMatUS: Pruebas en Lean de la reflexividad de la inclusión de conjuntos
• ForMatUS: Pruebas en Lean del desarrollo de un producto de dos sumas
• ForMatUS: Pruebas en Lean de (x + y) + z = (x + z) + y
• ForMatUS: Pruebas en Lean de y = x → y = z → x = z
• ForMatUS: Pruebas en Lean de la transitividad de la igualdad
• ForMatUS: Regla de eliminación de la igualdad en Lean
• ForMatUS: Pruebas en Lean de ∃x∃y P(x,y) ↔ ∃y∃x P(x,y)
• ForMatUS: Pruebas en Lean de ∃x (P(x) ∨ Q(x)) ↔ ∃x P(x) ∨ ∃x Q(x)
• ForMatUS: Pruebas en Lean de ∀x (P(x) ∧ Q(x)) ↔ ∀x P(x) ∧ ∀x Q(x)
• ForMatUS: Pruebas en Lean de ¬∀x P(x) ↔ ∃x ¬P(x)
• ForMatUS: Regla de eliminación del cuantificador existencial en Lean
• ForMatUS: Regla de introducción del cuantificador existencial en Lean
• Resumen de lecturas compartidas durante septiembre de 2020
• ForMatUS: Regla de introducción del cuantificador universal en Lean
• ForMatUS: Regla de eliminación del cuantificador universal en Lean
• ForMatUS: Pruebas en Lean de ¬P → Q, ¬Q ⊢ P
• ForMatUS: Pruebas en Lean de P, ¬¬(Q ∧ R) ⊢ ¬¬P ∧ R
• ForMatUS: Pruebas en Lean de P → Q ⊢ ¬P ∨ Q
• ForMatUS: Pruebas en Lean del principio del tercio excluso
• ForMatUS: Pruebas en Lean de la eliminación de la doble negación
• ForMatUS: Pruebas en Lean de la regla de reducción al absurdo
• PFH: Programas, funciones y dibujos (Introducción a la programación funcional con CodeWorld/Haskell)
• ForMatUS: Reglas de eliminación del bicondicional en P ↔ Q, P ∨ Q ⊢ P ∧ Q
• ForMatUS: Pruebas en Lean de P ∧ Q ↔ Q ∧ P
• ForMatUS: Pruebas en Lean de ¬P ∨ Q ⊢ P → Q
• ForMatUS: Pruebas en Lean de P → (Q → P)
• ForMatUS: Pruebas de Q → R ⊢ P ∨ Q → P ∨ R
• ForMatUS: Pruebas en Lean de P ∨ Q ⊢ Q ∨ P
• ForMatUS: Regla de eliminación de la disyunción en Lean
• ForMatUS: Reglas de introducción de la disyunción en Lean
• ForMatUS: Pruebas en Lean de ¬Q → ¬P ⊢ P → ¬¬Q
• ForMatUS: Pruebas en Lean de P → (Q → R), P, ¬R ⊢ ¬Q
• ForMatUS: Pruebas en Lean de la regla de introducción de la doble negación
• ForMatUS: Pruebas en Lean de P → Q ⊢ ¬Q → ¬P
• ForMatUS: Pruebas en Lean de P, P → Q, P → (Q → R) ⊢ R
• ForMatUS: Pruebas en Lean del modus tollens: P → Q, ¬Q ⊢ ¬P
• ForMatUS: Pruebas del silogismo hipotético: P → Q, Q → R ⊢ P → R
• ForMatUS: Pruebas en Lean de P → Q, P → ¬Q ⊢ ¬P
• ForMatUS: Reglas de la negación en Lean
• ForMatUS: Pruebas en Lean de P ∧ Q → Q ∧ P
• ForMatUS: Reglas de la conjunción en Lean
• ForMatUS: Regla de introducción del condicional en Lean
• ForMatUS: Regla de eliminación del condicional en Lean
• ForMatUS: Presentación de “Lógica con Lean”
• PFH: Definiciones de tipos en Haskell
• Resumen de lecturas compartidas durante agosto de 2020
• PFH: Funciones de orden superior en Haskell (Parte 2 de 3): Plegados
• PFH: Funciones de orden superior en Haskell (Parte 1 de 3)
• ForMatUS: El máximo común divisor de m y n es igual a m si, y sólo si, m divide a n (en Lean)
• ForMatUS: Formulación equivalente de lemas con dos hipótesis
• ForMatUS: Conmutatividad de la conjunción en Lean
• ForMatUS: Conectivas y desigualdades en Lean
• PFH: Definiciones por recursión en Haskell (Parte 2 de 2)
• PFH: Definiciones por recursión en Haskell (Parte 1 de 2)
• PFH: Cifrado César en Haskell
• ForMatUS: Monotonía de la multiplicación por no positivo (en Lean)
• ForMatUS: Monotonía de la multiplicación por no negativo (en Lean)
• ForMatUS: Suma de desigualdades (en Lean)
• ForMatUS: Suma de no negativos (en Lean)
• ForMatUS: La suma de no negativos es expansiva (en Lean)
• ForMatUS: Monotonía de la suma por la derecha en Lean
• ForMatUS: Monotonía de la suma por la izquierda en Lean
• ForMatUS: Eliminación de la disyunción en Lean
• ForMatUS: Introducción de la conjunción en Lean
• ForMatUS: Eliminación de la conjunción en Lean
• PFH: Definiciones por comprensión en Haskell
• ForMatUS: Eliminación de la equivalencia en Lean
• ForMatUS: Introducción de la implicación en Lean
• ForMatUS: Eliminación de la implicación en Lean
• PFH: Métodos elementales de definición de funciones en Haskell
• PFH: Tipos y clases en Haskell
• PFH: Introducción a la programación funcional con Haskell (Parte 2 de 2)
• PFH: Haskell con JupyterLab
• PFH: Introducción a la programación funcional con Haskell (Parte 1 de 2)
• ForMatUS: Ejercicios con Lean sobre aritmética real
• ForMatUS: Prueba en Lean con hipótesis y uso de lemas
• ForMatUS: Prueba en Lean mediante encadenamiento de ecuaciones
• ForMatUS: Prueba en Lean, mediante reescritura, de la transitividad de la igualdad
• ForMatUS: Presentación de “DAO (Demostración Asistida por Ordenador) con Lean”
• ForMatUS: Libro “Matemáticas en Lean”
• Proyecto ForMatUS (Formalización de las Matemáticas de la US)
• Resumen de lecturas compartidas durante julio de 2020
• Resumen de lecturas compartidas durante junio de 2020
• Resumen de lecturas compartidas durante mayo de 2020
• LMF2019: Definiciones inductivas en Isabelle/HOL
• I1M2019: El tipo abstracto de datos de grafos en Haskell
• I1M2019: El patrón de búsqueda en escalada en Haskell
• LMF2019: Desarrollo de teorías formalizadas con Isabelle/HOL
• I1M2019: El patrón de búsqueda por primero el mejor en Haskell
• Vídeos de las clases de razonamiento automático con Isabelle/HOL
• Vídeos de las clases de algorítmica con Haskell
• I1M2019: El patrón de búsqueda en espacios de estados en Haskell
• LMF2019: Razonamiento sobre árboles y bosques en Isabelle/HOL
• I1M2019: Resolución de problemas mediante búsqueda en espacios de estados
• I1M2019: El patrón de divide y vencerás en Haskell
• LMF2019: Razonamiento por casos y por inducción en Isabelle/HOL
• I1M2019: Programación dinámica en Haskell
• Resumen de lecturas compartidas durante abril de 2020
• I1M2019: El TAD de los polinomios en Haskell (2)
• LMF2019: Razonamiento sobre programas con Isabelle/HOL (2º parte)
• I1M2019: El TAD de los polinomios en Haskell
• I1M2019: El TAD de los montículos en Haskell
• I1M2019: El TAD de los árboles binarios de búsqueda en Haskell
• LMF2019: Razonamiento sobre programas con Isabelle/HOL (1º parte)
• I1M2019: Las librerías de conjuntos y de diccionarios en Haskell
• I1M2019: El TAD de los conjuntos en Haskell
• LMF2019: Programación funcional con Isabelle/HOL
• I1M2019: Algoritmos de ordenación en Haskell
• I1M2019: El tipo abstracto de datos de las colas de prioridad en Haskell
• Resumen de lecturas compartidas durante marzo de 2020
• I1M2019: El tipo abstracto de datos de las colas en Haskell
• I1M2019: El tipo abstracto de datos de las pilas en Haskell
• LMF2019: Deducción natural en lógica de primer orden (2/2)
• I1M2019: Análisis de la complejidad de los algoritmos
• I1M2019: Distancia esperada entre dos puntos de un cuadrado unitario
• LMF2019: Deducción natural en lógica de primer orden (1/2)
• I1M2019: Cálculo del número pi mediante el método de Montecarlo
• I1M2019: Aleatoriedad en Haskell
• Resumen de lecturas compartidas del 1 al 7 de marzo de 2020
• I1M2019: Combinatoria en Haskell
• LMF2019: Sintaxis y semántica de la lógica de primer orden
• I1M2019: Cálculo simbólico con Maxima
• LMF2019: Ejercicios de deducción natural con Isabelle/HOL (2)
• Resumen de lecturas compartidas durante febrero de 2020
• Reseña: Graph theory in Coq: minors, treewidth, and isomorphisms
• Resumen de lecturas compartidas del 22 al 29 de febrero de 2020
• LMF2019: Deducción natural proposicional (2)
• I1M2019: Introducción a la programación imperativa con Maxima
• I1M2019: Introducción al cálculo simbólico con Maxima
• LMF2019: Ejercicios de deducción natural con Isabelle/HOL (1)
• Reseña: Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi
• Resumen de lecturas compartidas del 16 al 21 de febrero de 2020
• I1M2019: Cálculo numérico en Haskell
• LMF2019: Deducción natural proposicional (1)
• I1M2019: Las librerías de vectores y matrices en Haskell
• LMF2019: Ejercicios de sintaxis y semántica de la lógica proposicional
• Reseña: Mac Lane’s comparison theorem for the Kleisli construction formalized in Coq
• Resumen de lecturas compartidas del 9 al 15 de febrero de 2020
• I1M2019: Ejercicios sobre vectores y matrices en Haskell
• RA2019: Verificación de la ordenación por inserción con Isabelle/HOL
• RA2019: Demostración en Isabelle de la corrección de un compilador
• LMF2019: Sintaxis y semántica de la lógica proposicional
• I1M2019: Matrices en Haskell
• LMF2019: Presentación del curso de “Lógica matemática y fundamentos”
• Resumen de lecturas compartidas del 1 al 8 de febrero de 2020
• Reseña: A comprehensive framework for saturation theorem proving
• LMF2019: Comienzo del curso
• RA2019: Reducción de SAT a Clique en Haskell
• RA2019: El algoritmo de Davis-Putnam en Haskell
• Resumen de lecturas compartidas durante enero de 2020
• Reseña: A formalised polynomial-time reduction from 3SAT to Clique
• Resumen de lecturas compartidas del 25 al 31 de enero de 2020
• RA2019: SAT (solving)
• Reseña: A formal proof of the irrationality of ζ(3)
• Resumen de lecturas compartidas del 19 al 24 de enero de 2020
• I1M2019: 3º examen de programación funcional con Haskell
• Reseña: The space of mathematical software systems
• Resumen de lecturas compartidas del 12 al 18 de enero de 2020
• RA2019: Deducción natural de primer orden con Isabelle/HOL
• Reseña: “Proof pearl: Braun trees”
• Resumen de lecturas compartidas del 1 al 11 de enero de 2020
• I1M2019: El juego de la vida en Haskell
• RA2019: Sintaxis y semántica de la lógica de primer orden
• I1M2019: Manejo de ficheros en Haskell
• I1M2019: Representación gráfica de funciones en Haskell con GNUplot
• I1M2019: Programas interactivos en Haskell
• Resumen de lecturas compartidas durante diciembre de 2019
• I1M2019: El problema de Hamming en Haskell
• I1M2019: El problema de las N reinas en Haskell
• I1M2019: Problema del concurso “Cifras y letras” en Haskell
• RA2019: Deducción natural proposicional con Isabelle/HOL (2)
• I1M2019: 2º examen de programación funcional con Haskell
• I1M2019: Ejercicios de evaluación perezosa y listas infinitas en Haskell
• RA2019: Deducción natural proposicional con Isabelle/HOL (1)
• I1M2019: Problemas de Exercitium del 22 y 29 de noviembre
• I1M2019: Evaluación perezosa en Haskell
• RA2019: Ejercicios de cuantificadores sobre listas en Isabelle/HOL
• RA2019: Razonamiento sobre árboles y bosques en Isabelle/HOL
• I1M2019: Problemas de Exercitium del 20 y 21 de noviembre
• I1M2019: Definiciones de clases en Haskell
• I1M2019: Programa en Haskell para reconocer tautologías
• Resumen de lecturas compartidas durante noviembre de 2019
• I1M2019: Introducción a la programación imperativa con Python
• I1M2019: Ejercicios sobre árboles binarios en Haskell
• RA2019: Ejercicios de razonamiento estructurado sobre programas en Isabelle/HOL
• RA2019: Razonamiento por casos y por inducción en Isabelle/HOL
• I1M2019: Problemas de Exercitium del 18 y 19 de noviembre
• I1M2019: De la matemática a la máquina
• I1M2019: Problemas de Exercitium del 14 y 15 de noviembre
• I1M2019: Definiciones de tipos en Haskell
• RA2019: Razonamiento estructurado sobre programas con Isabelle/HOL
• RA2019: Ejercicios de razonamiento sobre programas en Isabelle/HOL
• I1M2019: Problemas de Exercitium del 11 al 13 de noviembre
• I1M2019: Codificación binaria y transmisión de cadenas en Haskell