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