{"id":1811,"date":"2012-01-08T07:30:25","date_gmt":"2012-01-08T07:30:25","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1811"},"modified":"2013-03-08T05:48:56","modified_gmt":"2013-03-08T05:48:56","slug":"lecturas-del-grupo-de-logica-computacional-enero-de-2012","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lecturas-del-grupo-de-logica-computacional-enero-de-2012\/","title":{"rendered":"Lecturas del Grupo de L\u00f3gica Computacional (Enero de 2012)"},"content":{"rendered":"

Esta entrada es una recopilaci\u00f3n de lecturas compartidas en la lista de correo del grupo de l\u00f3gica computacional<\/a> desde el 1 de Octubre de 2011 hasta el 7 de Enero de 2012. La anterior recopilaci\u00f3n fue la de Septiembre de 2011<\/a>\n<\/p>\n

\nLa recopilaci\u00f3n est\u00e1 ordenada por la fecha de su publicaci\u00f3n en la lista. Al final de cada art\u00edculo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.\n<\/p>\n

<\/p>\n

    \n
  1. \nAutomated reasoning: some successes and new challenges<\/a>. #RA\n<\/li>\n
  2. \nGeneralized and formalized uncurrying<\/a>. #Isabelle\n<\/li>\n
  3. \nBasic first-order model theory in Mizar<\/a>. #Mizar\n<\/li>\n
  4. \nA certified module to study digital images with the Kenzo system<\/a>. #ACL2\n<\/li>\n
  5. \nWhat is a proof?<\/a>\n<\/li>\n
  6. \nLos peligros de \u201cpagar por publicar\u201d en las revistas cient\u00edficas de acceso abierto<\/a>.\n<\/li>\n
  7. \nThe dangers of the \u201cauthor pays\u201d model in mathematical publishing<\/a>.\n<\/li>\n
  8. \nProof Pearl: The marriage theorem<\/a>. #Isabelle\n<\/li>\n
  9. \n“Algorithms” is not a four-letter word<\/a>. #Algor\u00edtmica\n<\/li>\n
  10. \nAn overview of methods for large-theory automated theorem proving<\/a> #DAT.\n<\/li>\n
  11. \nLecturas del Grupo de L\u00f3gica Computacional (Septiembre de 2011)<\/a>\n<\/li>\n
  12. \nHaskell tutorial for C programmers<\/a>. #Tutorial #Haskell\n<\/li>\n
  13. \nFormalisation des courbes elliptiques en Coq<\/a>. #Tesis #Coq\n<\/li>\n
  14. \nProgress report on the ARC Project: Creating logical models of Gothic catrals<\/a>. #IA #Prolog #RC\n<\/li>\n
  15. \nOCaml for the Masses: Why the next language you learn should be functional<\/a>. #FP\n<\/li>\n
  16. \nEfficient mergesort<\/a>. #Isabelle #AFP\n<\/li>\n
  17. \nFormalization of propositional linear temporal logic in the Mizar system<\/a>. #Mizar\n<\/li>\n
  18. \nVerification of certifying computations<\/a> #Isabelle\n<\/li>\n
  19. \nCoq, a proof assistant based on higher-order intuitionistic type theory<\/a>. #Coq\n<\/li>\n
  20. \nRetos y oportunidades de la IA en I+D+i con empresas<\/a>. #IA\n<\/li>\n
  21. \nCompositional verification of a communication protocol for a remotely operated vehicle<\/a>. #PVS\n<\/li>\n
  22. \nA definitional encoding of TLA* in Isabelle\/HOL<\/a>. #Isabelle\n<\/li>\n
  23. \nVerSAT: a verified modern SAT solver<\/a>. #GURU\n<\/li>\n
  24. \nTowards automated system synthesis using SCIDUCTION<\/a>. #Tesis\n<\/li>\n
  25. \nDecision procedures for program synthesis and verification<\/a>. #Tesis\n<\/li>\n
  26. \nGrid based propositional satisfiability solving<\/a>. #Tesis #SAT\n<\/li>\n
  27. \nPartial mutual exclusion for infinitely many processes<\/a>. #PVS\n<\/li>\n
  28. \nCertifying algorithms<\/a>. #Algoritmosfehacientes<\/sub>\n<\/li>\n
  29. \nA proof pearl with the fan theorem and bar induction (walking through infinite trees with mixed induction and coinduction)<\/a> #Coq\n<\/li>\n
  30. \nComplex systems: A survey<\/a>\n<\/li>\n
  31. \nWhat is mathematical logic? A survey<\/a>.\n<\/li>\n
  32. \nKnowledge representation and reasoning (Logic meets probability theory)<\/a> #Libro\n<\/li>\n
  33. \nConstruction des nombres alg\u00e9briques r\u00e9els en Coq<\/a>. #Coq\n<\/li>\n
  34. \nA methodology for the development and verification of expressive ontologies<\/a>. #Tesis #Prover9\n<\/li>\n
  35. \nWave equation numerical resolution: mathematics and program<\/a>. #Coq\n<\/li>\n
  36. \n\u00c9tude de la diff\u00e9rentiabilit\u00e9 et de l’int\u00e9grabilit\u00e9 en Coq (Application \u00e0 la formule de d’Alembert pour l’\u00e9quation des ondes)<\/a> #Coq\n<\/li>\n
  37. \nFormalizing a proof that e is transcendental<\/a>. #HOLLight<\/sub>\n<\/li>\n
  38. \nA proof-theoretic account of primitive recursion and primitive iteration<\/a>. #MinLog\n<\/li>\n
  39. \nInitial semantics for higher-order typed syntax in Coq<\/a>. #Coq\n<\/li>\n
  40. \nDesperately seeking mathematical truth<\/a>. #Filosofia\n<\/li>\n
  41. \nInteractive theorem proving (A survey\/tutorial, for logician)<\/a>. #Tutorial #ITP\n<\/li>\n
  42. \nCan the computer really help us to prove theorems?<\/a>. #ITP #Panorama\n<\/li>\n
  43. \nAn empirical study of errors in translating natural language into logic<\/a>. #MDE\n<\/li>\n
  44. \nThe hardest logic puzzle ever<\/a>. #Rompecabeza\n<\/li>\n
  45. \nL’ordinateur au c\u0153ur de la d\u00e9couverte math\u00e9matique<\/a>.\n<\/li>\n
  46. \n\u00daltimos dos d\u00edgitos de (1+5(2*n+1)<\/sup>)\/6<\/a>. #Haskell\n<\/li>\n
  47. \nDisparad contra la Ilustraci\u00f3n<\/a>.\n<\/li>\n
  48. \nOn the aesthetics of computer science<\/a>.\n<\/li>\n
  49. \nComputing with hereditarily finite sequences<\/a>. #Prolog #MKM\n<\/li>\n
  50. \nAn interview with Stephen A. Cook<\/a>\n<\/li>\n<\/ol>\n

    En Mendeley tambi\u00e9n se encuentran las lecturas del Grupo de L\u00f3gica Computacional<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"

    Esta entrada es una recopilaci\u00f3n de lecturas compartidas en la lista de correo del grupo de l\u00f3gica computacional desde el 1 de Octubre de 2011 hasta el 7 de Enero de 2012. La anterior recopilaci\u00f3n fue la de Septiembre de 2011 La recopilaci\u00f3n est\u00e1 ordenada por la fecha de su publicaci\u00f3n en la lista. Al…<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[177],"tags":[178,292],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1811"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=1811"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1811\/revisions"}],"predecessor-version":[{"id":2875,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1811\/revisions\/2875"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1811"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1811"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1811"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}