Lecturas del Grupo de Lógica Computacional (Septiembre de 2011)

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional. 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. Formalization of Abstract State Transition Systems for SAT. #Isabelle
  2. Zeno: A tool for the automatic verification of algebraic properties of functional programs #Isabelle #Haskell
  3. Automating Induction with an SMT Solver. #SMT #Z3
  4. Artificial Intelligence Techniques for Understanding Gothic Cathedrals #Prolog
  5. RDFS/OWL reasoning using the MapReduce framework. #DL #SW
  6. Automatic Proof and Disproof in Isabelle/HOL. #Isabelle
  7. Proof Pearl: Mechanizing the Textbook Proof of Huffman’s Algorithm. #Isabelle
  8. Isabelle Primer for Mathematicians. #Isabelle
  9. Majority Vote Algorithm Revisited Again #Isabelle
  10. A survey on Interactive Theorem Proving #Survey #ITP
  11. Formalization of Wu’s simple method in Coq. #Coq
  12. Functional Programming for Java Developers. #PF #Tutorial
  13. Formal Verification for Numerical Methods. #Tesis #Coq
  14. Practical Semantic Web and Linked Data Applications. Lisp Edition. #SW #Lisp
  15. Basics of Coq. #Coq #Tutorial
  16. Coq in a Hurry. #Coq #Tutorial
  17. Reasoning Processes in Propositional Logic.
  18. Programación Funcional con Haskell. #Haskell
  19. Ejercicios de programación funcional con Haskell. #Haskell
  20. Introducción a la programación lógica con Prolog. #Prolog
  21. Ejercicios de programación declarativa con Prolog. #Prolog
  22. Verification of the OWL-Time Ontology. #Prover9 #Ontología
  23. Proof Pearl: A Formal Proof of Higman’s Lemma in ACL2. #ACL2
  24. Apprendre Haskell vous fera le plus grand bien!. #Haskell
  25. Implementation of Bourbaki’s Elements of Mathematics in Coq: Part One, Theory of Sets. #Coq
  26. Defining and using deductive systems with Isabelle. #Isabelle
  27. Some Applications of Propositional Logic to Cellular Automata.
  28. Implementation of Bourbaki’s Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers. #Coq
  29. How Kenzo program works.

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

Lecturas del Grupo de Lógica Computacional (Agosto de 2011)

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional durante el mes de agosto 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. Theorem proving for verification (the early days) #Historia
  2. Selecting attributes for sport forecasting using formal concept analysis #AFC
  3. Lecturas del Grupo de Lógica Computacional (Julio de 2011). #GLC #Vestigium
  4. Formal methods: practice and experience #Métodos_formales
  5. Automated deduction for verification #DAT
  6. Software model checking #Model_checking
  7. The verified software initiative: A Manifesto #Verificación
  8. How can i do that with ACL2 recent enhancements to ACL2 #ACL2
  9. Algebraic proofs over noncommutative formulas #Cálculo_polinomial
  10. Studies in algebraic and propositional proof complexity #Tesis #Cálculo_polinomial
  11. Formalization of an Efficient Representation of Bernstein Polynomials and Applications to Global Optimization #PVS
  12. Automating Algebraic Methods in Isabelle #Isabelle
  13. A Repository for Tarski-Kleene Algebras #Isabelle
  14. Emergence and refinement #Emergencia #Refinamentos
  15. Automated Proving in Geometry using Gröbner Bases in Isabelle/HOL #Isabelle
  16. How Efficient Can Fully Verified Functional Programs Be – A Case Study of Graph Traversal Algorithms #Isabelle
  17. Imperative functional programming with Isabelle/HOL #Isabelle
  18. A Flexible Formal Verification Framework for Industrial Scale Validation #ACL2
  19. Markets are Efficient if and Only if P = NP.
  20. Bit-Blasting ACL2 Theorems #ACL2 #GL
  21. A Verified Framework for Symbolic Execution in the ACL2 Theorem Prover. #ACL2 #GL
  22. Integrating Testing and Interactive Theorem Proving #ACL2
  23. seL4 Enforces Integrity #Isabelle
  24. Peirce’s Truth-functional Analysis and the Origin of Truth Tables. #Historia
  25. Towards Flight Control Verification Using Automated Theorem Proving #MetiTarski
  26. Ott: Effective tool support for the working semanticist. #Ott #Coq #Isabelle #HOL
  27. Lightweight Tools for Heavyweight Semantics. #Lem #Ott #Coq #Isabelle #HOL
  28. Verifying SAT and SMT in Coq for a fully automated decision procedure. #Coq #SAT #SMT
  29. Maximum Cardinality Matching. #Isabelle
  30. Premise Selection for Mathematics by Corpus Analysis and Kernel Methods. #AA
  31. Gauss-Jordan Elimination for Matrices Represented as Functions. #Isabelle
  32. Verification of Dependable Software using Spark and Isabelle. #Isabelle
  33. Verification of Programs in Virtual Memory Using Separation Logic. #Isabelle
  34. Automated Specification Analysis Using an Interactive Theorem Prover. #ACL2
  35. Formal Analysis of Fractional Order Systems in HOL. #HOL

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

Lecturas del Grupo de Lógica Computacional (Julio de 2011)

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional. 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. Razonamiento formalizado para la enseñanza de las matemáticas. [#Vestigium, #Enseñanza]
  2. The Ideal Mathematician. [#Humor]
  3. El problema de las puertas en Haskell. [#Haskell]
  4. Metadata for a mathematical wiki: Initial experiments. [#Mizar]
  5. Logical Verification. [#Coq]
  6. Formal proofs for theoretical properties of Newton’s method. [#Coq]
  7. Formalisation de la logique de description ALC dans l’assistant de preuve Coq. [#Coq, #ALC]
  8. Vérification d’une méthode de preuve pour la logique de description ALC. [#Isabelle. #ALC]
  9. A critique of Abelson and Sussman or why calculating is better than scheming. [#Haskell, #Lisp]
  10. Experiments with computable matrices in the Coq system. [#Coq]
  11. Computing the homology of groups: the geometric way. [#Kenzo]
  12. Peut-on faire des mathématiques avec un ordinateur?. [#Matemática computacional]
  13. The Theory Behind TheoryMind. [#Isabelle]
  14. Provably correct conflict prevention bands algorithms. [#PVS]
  15. Peut-on avoir confiance en l’informatique?. [#Verificación]
  16. Lecturas de razonamiento formalizado (del 27-Oct-2010 al 1-Jul-2011). [#GLC, #Vestigium]
  17. Automated theorem provers a practical tool for the working mathematician. [#DAO, #Vestigium]
  18. Intellectual Freedom. [#Humor]
  19. Ciencia china ‘duplicada’ en Galicia. [#Sociología]
  20. Expresiones aritméticas mediante tipos abstracto de datos y polinomios. [#Haskell, #Vestigium]
  21. A verified runtime for a verified theorem prover. [#ACL2]
  22. A Framework for Automated and Certified Refinement Steps. [#Isabelle]
  23. Descomposiciones en sumas de cuadrados en Haskell. [#Haskell, #Vestigium]
  24. Interactive Proof Introduction to IsabelleHOL. [#Isabelle]
  25. Coq au vin (The Coq proof assistant and the Curry-Howard correspondence) [#Coq]
  26. Hardware languages and proof. [#Tesis, #PVS, #SAL]