I1M2011: Definición de tipos de datos en Haskell

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado la definición de nuevos tipos de datos y de funciones sobre dichos tipos. Concretamente, se ha estudiado

  • cómo definir tipos usando type,
  • cómo definir funciones con dominio o rango en tipos definidos usando type,
  • cómo definir tipos usando data,
  • cómo definir funciones con dominio o rango en tipos definidos usando
  • data y

  • cómo definir tipos de datos recursivos usando como ejemplo los naturales.

Las transparencias usadas en la clase son las del tema 9:
Read More “I1M2011: Definición de tipos de datos en Haskell”

RA2011: Patrones de inducción en Isabelle: casos, inducción y otros

En la clase de hoy del curso de Razonamiento automático se han presentado los principales patrones de inducción en Isabelle: en la primera parte se ha presentado los patrones de de mostración por casos y por inducción y en la segunda parte se han presentado otros patrones (eliminación de disyunción, negación, contradicción y equivalencias).

La primera parte de la clase se ha basado en la siguiente teoría Isabelle
Read More “RA2011: Patrones de inducción en Isabelle: casos, inducción y otros”

Lecturas del Grupo de Lógica Computacional (Enero de 2012)

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional durante el mes de Enero 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. L’ordinateur au cœur de la découverte mathématique. #Divulgación
  2. Últimos dos dígitos de (1+5^(2n+1))/6. #Haskell
  3. Disparad contra la Ilustración. #Enseñanza
  4. On the aesthetics of computer science. #Divulgación
  5. Computing with hereditarily finite sequences. #Prolog #MKM
  6. An interview with Stephen A. Cook. #Divulgación
  7. Markov models. #Isabelle
  8. Turing machines por J. Hopcroft #Clásico #Divulgación
  9. The way forward for Computer Science in the U.K. #Enseñanza
  10. Teaching semantics with a proof assistant: No more LSD trip proofs. #Enseñanza #Lógica #Isabelle
  11. Enseñando deducción natural con Coq. #Enseñanza #Lógica #Coq
  12. Formalisation en OWL pour vérifier les spécifications d’un environnement intelligent. #OWL #Prover9
  13. Think complexity. #Sistemas_complejos #Python
  14. Algorithmic graph theory. #Libro #Algorítmica #Sage
  15. A simplified framework for first-order languages and its formalization in Mizar. #Tesis #Metalógica #Mizar
  16. ProofPeer – A cloud-based interactive theorem proving system. #ProofPeer
  17. Generic proof tools and finite group theory. #Tesis #Coq

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