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 desde el 1 de Octubre de 2011 hasta el 7 de Enero de 2012. La anterior recopilación fue la de Septiembre de 2011

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. Automated reasoning: some successes and new challenges. #RA
  2. Generalized and formalized uncurrying. #Isabelle
  3. Basic first-order model theory in Mizar. #Mizar
  4. A certified module to study digital images with the Kenzo system. #ACL2
  5. What is a proof?
  6. Los peligros de “pagar por publicar” en las revistas científicas de acceso abierto.
  7. The dangers of the “author pays” model in mathematical publishing.
  8. Proof Pearl: The marriage theorem. #Isabelle
  9. “Algorithms” is not a four-letter word. #Algorítmica
  10. An overview of methods for large-theory automated theorem proving #DAT.
  11. Lecturas del Grupo de Lógica Computacional (Septiembre de 2011)
  12. Haskell tutorial for C programmers. #Tutorial #Haskell
  13. Formalisation des courbes elliptiques en Coq. #Tesis #Coq
  14. Progress report on the ARC Project: Creating logical models of Gothic catrals. #IA #Prolog #RC
  15. OCaml for the Masses: Why the next language you learn should be functional. #FP
  16. Efficient mergesort. #Isabelle #AFP
  17. Formalization of propositional linear temporal logic in the Mizar system. #Mizar
  18. Verification of certifying computations #Isabelle
  19. Coq, a proof assistant based on higher-order intuitionistic type theory. #Coq
  20. Retos y oportunidades de la IA en I+D+i con empresas. #IA
  21. Compositional verification of a communication protocol for a remotely operated vehicle. #PVS
  22. A definitional encoding of TLA* in Isabelle/HOL. #Isabelle
  23. VerSAT: a verified modern SAT solver. #GURU
  24. Towards automated system synthesis using SCIDUCTION. #Tesis
  25. Decision procedures for program synthesis and verification. #Tesis
  26. Grid based propositional satisfiability solving. #Tesis #SAT
  27. Partial mutual exclusion for infinitely many processes. #PVS
  28. Certifying algorithms. #Algoritmosfehacientes
  29. A proof pearl with the fan theorem and bar induction (walking through infinite trees with mixed induction and coinduction) #Coq
  30. Complex systems: A survey
  31. What is mathematical logic? A survey.
  32. Knowledge representation and reasoning (Logic meets probability theory) #Libro
  33. Construction des nombres algébriques réels en Coq. #Coq
  34. A methodology for the development and verification of expressive ontologies. #Tesis #Prover9
  35. Wave equation numerical resolution: mathematics and program. #Coq
  36. Étude de la différentiabilité et de l’intégrabilité en Coq (Application à la formule de d’Alembert pour l’équation des ondes) #Coq
  37. Formalizing a proof that e is transcendental. #HOLLight
  38. A proof-theoretic account of primitive recursion and primitive iteration. #MinLog
  39. Initial semantics for higher-order typed syntax in Coq. #Coq
  40. Desperately seeking mathematical truth. #Filosofia
  41. Interactive theorem proving (A survey/tutorial, for logician). #Tutorial #ITP
  42. Can the computer really help us to prove theorems?. #ITP #Panorama
  43. An empirical study of errors in translating natural language into logic. #MDE
  44. The hardest logic puzzle ever. #Rompecabeza
  45. L’ordinateur au cœur de la découverte mathématique.
  46. Últimos dos dígitos de (1+5(2*n+1))/6. #Haskell
  47. Disparad contra la Ilustración.
  48. On the aesthetics of computer science.
  49. Computing with hereditarily finite sequences. #Prolog #MKM
  50. An interview with Stephen A. Cook

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