{"id":2463,"date":"2013-01-07T22:13:20","date_gmt":"2013-01-07T22:13:20","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2463"},"modified":"2013-03-08T05:47:35","modified_gmt":"2013-03-08T05:47:35","slug":"lecturas-del-grupo-de-logica-computacional-diciembre-de-2012","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lecturas-del-grupo-de-logica-computacional-diciembre-de-2012\/","title":{"rendered":"Lecturas del Grupo de L\u00f3gica Computacional (Diciembre 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> durante el mes de diciembre de 2012. La anterior recopilaci\u00f3n fue la de noviembre de 2012<\/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

    \n
  1. Verifying probabilistic correctness in Isabelle with pGCL<\/a>. #Isabelle\n<\/li>\n
  2. Formalization of a strategy for the KRK chess endgame<\/a>. #Coq\n<\/li>\n
  3. Formalization and implementation of algebraic methods in Geometry<\/a>. #Isabelle\n<\/li>\n
  4. Formal verification of conflict detection algorithms for arbitrary trajectories<\/a>. #PVS\n<\/li>\n
  5. Learning-assisted automated reasoning with Flyspeck<\/a>. #Mizar\n<\/li>\n
  6. Deductive formal verification of embedded systems<\/a>. #Tesis #Coq\n<\/li>\n
  7. Verification of redecoration for infinite triangular matrices using coinduction<\/a>. #Coq\n<\/li>\n
  8. Repr\u00e9sentation coinductive des graphes<\/a>. #Tesis #Coq\n<\/li>\n
  9. Formal mathematics for mathematicians<\/a>.\n<\/li>\n
  10. The HOL Light theory of euclidean space<\/a>. #HOLLight<\/sub>\n<\/li>\n
  11. Formalization of definitions and theorems related to an elliptic curve over a finite prime field by using Mizar<\/a>. #Mizar\n<\/li>\n
  12. The G\u00f6del completeness theorem for uncountable languages<\/a>. #Mizar\n<\/li>\n
  13. Machine learning in Proof General: Interfacing interfaces<\/a>. #Coq\n<\/li>\n
  14. Interactive verification of Markov chains: Two distributed protocol case studies<\/a>. #Isabelle\n<\/li>\n
  15. Du r\u00eave \u00e0 la r\u00e9alit\u00e9 des preuves<\/a>. (Interstices, 2012) #Divulgaci\u00f3n #DAO\n<\/li>\n
  16. Interactive theorem proving, automated reasoning, and mathematical computation<\/a>\n<\/li>\n<\/ol>\n

    \nEn 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 durante el mes de diciembre de 2012. La anterior recopilaci\u00f3n fue la de noviembre de 2012. La recopilaci\u00f3n est\u00e1 ordenada por la fecha de su publicaci\u00f3n en la lista. Al final de cada art\u00edculo se encuentra etiquetas…<\/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":[1],"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\/2463"}],"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=2463"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2463\/revisions"}],"predecessor-version":[{"id":2709,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2463\/revisions\/2709"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2463"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2463"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2463"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}