I1M2012: Número con mayor cantidad de divisores

En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado la solución con Haskell de un problema propuesto para la Olimpiada Internacional de Matemáticas de 1983. Su enunciado es

”¿Cuál de los números 1, 2, …, 1983 tiene mayor número de divisores?”

Se van a presentar distintas soluciones y comparar sus eficiciencias. La primera definición es

donde (divisores1 n) es el conjunto de los divisores de n.

El cálculo con la primera definición es

En la segunda definición se cambia la definición de divisores

El cálculo con la segunda definición es

En la tercera definición se ordenan los pares

El cálculo con la tercera definición es

Se observa que el tiempo se ha reducido de 9.00 segundos a 2.76.

I1M2011: Ejercicios de definiciones por recursión y comprensión en Haskell (2)

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones de los ejercicios 8 a 13 de la 9ª relación en la que se presentan ejercicios con dos definiciones (una por recursión y otra por comprensión) y la comprobación de la equivalencia de las dos definiciones con QuickCheck.

Los ejercicios, y sus soluciones, se muestran a continuación:
Read More “I1M2011: Ejercicios de definiciones por recursión y comprensión en Haskell (2)”

Lecturas del Grupo de Lógica Computacional (Septiembre-Noviembre de 2012)

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional desde el mes de septiembre de 2012. La anterior recopilación fue la de agosto de 2012.

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. Operational refinement for compiler correctness. #Tesis #Coq
  2. Interactive and automated proofs for graph transformations. #Isabelle
  3. Lecturas del Grupo de Lógica Computacional (Marzo-Agosto de 2012)
  4. Piensa en Haskell (Ejercicios de programación funcional con Haskell). #Haskell
  5. ¿Computadores von Neumann, o computadores Turing? #Historia
  6. Formalizing Frankl’s conjecture: FC-families. #Isabelle
  7. Implementing an efficient theorem prover. #Tesis #Vampire
  8. System of logic based on ordinals. #Tesis #Historia
  9. Proving concurrent noninterference (código) #Isabelle
  10. Improving real analysis in Coq: a user-friendly approach to integrals and derivatives. #Coq (CPP2012)
  11. Computing persistent homology within Coq/SSReflect. #Coq
  12. Software libre para una sociedad libre. #Libro #Pensamiento
  13. A formal proof of Sasaki-Murao algorithm. #Coq (MAP2012, code, Presentación).
  14. Confluence by decreasing diagrams formalized. #Isabelle
  15. Proof Pearl – A mechanized proof of GHC’s mergesort. #Isabelle #Haskell
  16. A logic-algebraic approach to decision taking in a railway interlocking system. #BG
  17. Scheme in industrial automation. #Scheme
  18. Parallelizing an interactive theorem prover: Functional programming and proofs with ACL2. #ACL2 #Tesis
  19. A string of pearls: Proofs of Fermat’s little theorem. #HOL4
  20. A formally-verified C compiler supporting floating-point arithmetic. #Coq
  21. The Boyer-Moore waterfall model revisited. #HOL_Light
  22. A Python pattern matcher project for an introduction to Artificial Intelligence course. #IA
  23. Informatik 2: Functional Programming. #Haskell
  24. Contributions to the formal verification of arithmetic algorithms. #Tesis #Coq
  25. Why learn Haskell?. #Tutorial #Haskell
  26. A mechanical verification of the independence of Tarski’s euclidean axiom y código #Tesina #Isabelle
  27. Weak completeness theorem for propositional linear time temporal logic. #Mizar
  28. Natural language processing for the working programmer. #Haskell #IA
  29. Nexus authorization logic (NAL): Logical results. #Coq
  30. Reasons for studying Haskell in University. #Haskell
  31. Constructive completeness for modal logic with transitive closure. #Coq #Modal
  32. A functional programming approach to AI search algorithms. #IA #PF
  33. Dual multi-adjoint concept lattices. #AFC
  34. Temas de “Demostración asistida por ordenador”. #Isabelle #Tutorial
  35. Verificación de programas: Introducción. #Verificación
  36. Último dígito del producto de números de Fermat. #Haskell #IMO
  37. A formal proof of square root and division elimination in embedded programs. #PVS
  38. Coq et caractères (Preuve formelle du théorème de Feit et Thompson). #Coq #Divulgación
  39. Formalized algebraic numbers: construction and first order theory. #Tesis #Coq
  40. How enterprises use functional languages, and why they don’t. #PF
  41. Inductive analysis of security protocols in Isabelle/HOL with applications to electronic voting. #Tesis #Isabelle
  42. Constructive formalization of regular languages. #Tesina #Coq
  43. Computing with free algebras. #Haskell
  44. Ask-Elle: a Haskell Tutor. #Tesis #Haskell #TI
  45. Using Isabelle to verify special relativity, with application to hypercomputation theory. #Isabelle

En Mendeley también se encuentran las lecturas del Grupo de Lógica Computacional.

I1M2011: Ejercicios de definiciones por recursión y comprensión en Haskell (1)

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones de los 7 primeros ejercicios de la 9ª relación en la que se presentan ejercicios con dos definiciones (una por recursión y otra por comprensión) y la comprobación de la equivalencia de las dos definiciones con QuickCheck.

Los ejercicios, y sus soluciones, se muestran a continuación:
Read More “I1M2011: Ejercicios de definiciones por recursión y comprensión en Haskell (1)”

LI2012: Sintaxis y semántica de la lógica de primer orden

En la clase de hoy del curso Lógica Informática se presentado la sintaxis y la semántica de la lógica de primer orden como respuestas a las siguientes preguntas: ¿qué es una fórmula?, ¿qué significa que una fórmula verdadera?

En primer lugar, a partir de los ejemplos de representación del conocimiento de la clase anterior, se han definido los símbolos lógicos (variables, conectivas, cuantificadores e igualdad) y los símbolos no lógicos (constantes, predicados y funciones) que forman el alfabeto del lenguaje de la lógica de primer orden.

A partir del alfabeto, se definen los términos, las fórmulas atómicas y las fórmulas del lenguaje.

Como medio del reconocimiento de fórmulas, se introducen los árboles de análisis. Con ello, respondemos a la primera de las preguntas iniciales.

En el estudio sintáctico, definimos el conjunto de las subfórmulas, el conjunto de las variables de un término, las ocurrencias libres y ligadas, el conjunto de las variables libres y ligadas y las fómulas cerradas y abiertas. Algunas de las definiciones anteriores se realizan por recursión sobre fórmulas o sobre términos.

En segundo lugar hemos esudiado la semántica, comenzando con distintas cuestiones sobre qué significa que una fórmula sea verdadera para resaltar su dependencia del universo, la interpretación de los símbolos no lógico y de las asignaciones a las variables libres.

Se han definido las estructuras de un lenguaje, las asignaciones a las variables y las interpretaciones de un lenguaje.

Se ha definido el valor de un término o de una fórmula en una interpretación. Con ello, repondemos a la segunda de las preguntas iniciales.

Las transparencias de esta clase son las páginas 11 a 34 del tema 7:
Read More “LI2012: Sintaxis y semántica de la lógica de primer orden”