Lecturas del Grupo de Lógica Computacional (Julio de 2011)

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional. La recopilación está ordenada por la fecha de su publicación en la lista. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.

  1. Razonamiento formalizado para la enseñanza de las matemáticas. [#Vestigium, #Enseñanza]
  2. The Ideal Mathematician. [#Humor]
  3. El problema de las puertas en Haskell. [#Haskell]
  4. Metadata for a mathematical wiki: Initial experiments. [#Mizar]
  5. Logical Verification. [#Coq]
  6. Formal proofs for theoretical properties of Newton’s method. [#Coq]
  7. Formalisation de la logique de description ALC dans l’assistant de preuve Coq. [#Coq, #ALC]
  8. Vérification d’une méthode de preuve pour la logique de description ALC. [#Isabelle. #ALC]
  9. A critique of Abelson and Sussman or why calculating is better than scheming. [#Haskell, #Lisp]
  10. Experiments with computable matrices in the Coq system. [#Coq]
  11. Computing the homology of groups: the geometric way. [#Kenzo]
  12. Peut-on faire des mathématiques avec un ordinateur?. [#Matemática computacional]
  13. The Theory Behind TheoryMind. [#Isabelle]
  14. Provably correct conflict prevention bands algorithms. [#PVS]
  15. Peut-on avoir confiance en l’informatique?. [#Verificación]
  16. Lecturas de razonamiento formalizado (del 27-Oct-2010 al 1-Jul-2011). [#GLC, #Vestigium]
  17. Automated theorem provers a practical tool for the working mathematician. [#DAO, #Vestigium]
  18. Intellectual Freedom. [#Humor]
  19. Ciencia china ‘duplicada’ en Galicia. [#Sociología]
  20. Expresiones aritméticas mediante tipos abstracto de datos y polinomios. [#Haskell, #Vestigium]
  21. A verified runtime for a verified theorem prover. [#ACL2]
  22. A Framework for Automated and Certified Refinement Steps. [#Isabelle]
  23. Descomposiciones en sumas de cuadrados en Haskell. [#Haskell, #Vestigium]
  24. Interactive Proof Introduction to IsabelleHOL. [#Isabelle]
  25. Coq au vin (The Coq proof assistant and the Curry-Howard correspondence) [#Coq]
  26. Hardware languages and proof. [#Tesis, #PVS, #SAL]

Una cuestión de unos y ceros

PorJosé A. Alonso

Esta relación de ejercicios, para la asignatura de Informática de 1º del Grado en Matemáticas, se basa en el problema 15 de los desafíos matemáticos de El País titulado Una cuestión de unos y ceros cuyo enunciado es el siguiente

El problema de esta semana parte de la observación de que todos los números naturales tienen al menos un múltiplo no nulo que está formado solamente por ceros y unos. (Por ejemplo: 1×10=10; 2×5=10; 3×37=111; 4X25=100; 5X2=10; 6X185=1110; 7×143=1001; 8X125=1000; 9×12345679=111111111… y así para cualquier número natural). La pregunta de la semana es: ¿por qué sucede esto?

La relación de ejercicios es la siguiente
Read More “Una cuestión de unos y ceros”

Enumeraciones de los números racionales en Haskell

PorJosé A. Alonso

He publicado en LógicaMente una relación de ejercicios en Haskell sobre enumeraciones de los números racionales, cuyo contenido es el siguiente.

El objetivo de esta relación es construir dos enumeraciones de los números racionales. Concretamente,

  • una enumeración basada en las representaciones hiperbinarias y
  • una enumeración basada en los los árboles de Calkin-Wilf.

También se incluye la comprobación de la igualdad de las dos sucesiones y una forma alternativa de calcular el número de representaciones hiperbinarias mediante la función fucs.

Esta relación se basa en los siguientes artículos:

La relación de ejercicios es
Read More “Enumeraciones de los números racionales en Haskell”

Interactive Proof: Introduction to Isabelle/HOL

PorJosé A. Alonso

Tobias Nipkow ha publicado un nuevo tutorial de Isabell/HOL: Interactive Proof: Introduction to Isabelle/HOL, que presentará a principio de agosto en la Summer School Marktoberdorf 2011.

El contenido del tutorial es el siguiente:

  • Elementos básicos de Isabelle/HOL: los tipos, términos, fórmulas y teorías.
  • Isabelle/HOL como lenguaje funcional verificable. En esta sección, presenta los tipos básicos (bool, nat y list), cómo pueden definirse funciones y tipos y cómo pueden demostrarse propiedades por inducción y simplificación.
  • Lógica y automatización de las demostraciones. En esta sección, presenta cómo se trabaja con fórmulas y conjuntos, cómo puede automatizarse las demostraciones de sus propiedades y cómo pueden analizarse las demostraciones en pasos elementales.
  • Demostraciones estructuradas con Isar. En esta sección, presenta ejemplos de demostraciones en Isar, patrones de demostraciones, técnicas para mejorar demostraciones y demostraciones por inducción y casos en Isar.

La presentación del tutorial está basada en ejemplos: se concentra en ejemplos que presenta los casos típicos sin explicar el caso general si se puede inferir de los ejemplos.

Las teorías que sirven de ejemplo del tutorial son las siguientes: Overview, Nat, List, Tree, Simp, Induct, Auto_Proof_Demo, Single_Step_Demo, Inductive_Demo, Isar_Demo, Isar_Induct_Demo.

El resto del material utilizado se encuentra en MOD2011.

Descomposiciones en sumas de cuadrados en Haskell

PorJosé A. Alonso

Esta relación de ejercicios, para la asignatura de Informática de 1º del Grado en Matemáticas, se basa en el problema 19 de los desafíos matemáticos de El País titulado Cuadrados que suman grandes cifras cuyo enunciado es el siguiente

Los números cuadrados (o cuadrados perfectos) son los cuadrados de los números naturales, es decir: 1 (1^2), 4 (2^2), 9 (3^2), 16 (4^2), 25 (5^2), etcétera. En el problema de esta semana trataremos de descubrir de cuántas maneras distintas se puede escribir un número dado como suma de cuatro cuadrados. Por ejemplo, el número 39 se puede escribir de dos formas: 39=1+1+1+36 y 39=1+4+9+25. Observemos que se pueden repetir sumandos y que no contaremos como maneras distintas de escritura las que se obtienen al cambiar el orden de los sumandos.

Las preguntas concretas son: ¿De cuántas formas distintas se puede escribir 2^2012 como suma de cuatro cuadrados? ¿Y de cuántas formas se puede escribir 2^2011?

La relación de ejercicios es la siguiente
Read More “Descomposiciones en sumas de cuadrados en Haskell”