Lecturas del Grupo de Lógica Computacional (Diciembre 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 diciembre de 2012. La anterior recopilación fue la de noviembre 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.
- Verifying probabilistic correctness in Isabelle with pGCL. #Isabelle
- Formalization of a strategy for the KRK chess endgame. #Coq
- Formalization and implementation of algebraic methods in Geometry. #Isabelle
- Formal verification of conflict detection algorithms for arbitrary trajectories. #PVS
- Learning-assisted automated reasoning with Flyspeck. #Mizar
- Deductive formal verification of embedded systems. #Tesis #Coq
- Verification of redecoration for infinite triangular matrices using coinduction. #Coq
- Représentation coinductive des graphes. #Tesis #Coq
- Formal mathematics for mathematicians.
- The HOL Light theory of euclidean space. #HOLLight
- Formalization of definitions and theorems related to an elliptic curve over a finite prime field by using Mizar. #Mizar
- The Gödel completeness theorem for uncountable languages. #Mizar
- Machine learning in Proof General: Interfacing interfaces. #Coq
- Interactive verification of Markov chains: Two distributed protocol case studies. #Isabelle
- Du rêve à la réalité des preuves. (Interstices, 2012) #Divulgación #DAO
- Interactive theorem proving, automated reasoning, and mathematical computation
En Mendeley también se encuentran las lecturas del Grupo de Lógica Computacional.