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.

Lógica Computacional en Sevilla (30 años en una hora)

PorJosé A. Alonso

Ayer, en las Jornadas de Lógica, Computación e Inteligencia Artificial, hice una presentación sobre el desarrollo de la investigación de la Lógica computacional en la Universidad de Sevilla desde sus comienzos (en el Seminario de Lógica Matemática del curso 1980-81) hasta la actualidad.

El título de la presentación fue Lógica Computacional en Sevilla (30 años en una hora).

Las transparencias usadas en la presentación son las que se muestran a continuación

Descargar (PDF, 1.6MB)

Certificación computacional del conocimiento matemático

PorJosé A. Alonso

Esta entrada está dedicada a los antecentes de la certificación computacional del conocimiento matemático en estilo declarativo.

Por lo que respecta a la verificación declarativa, sus raices se encuentran en el trabajo realizado en el proyecto Mizar. El proyecto Mizar comenzó en el 1973 como un intento de reconstruir la matemática en un entorno computacionalmente certificable. Los teoremas demostrados dentro del proyecto Mizar se encuentran fundamentalmente en la Mizar Mathematical Library y en la revista Formalized Mathematics que se publica desde el año 1990. El sistema Mizar no es automático sino que es sólo un verificador. Por contra, los sistemas de demostración no disponían de modos de demostración declararativa hasta que M. Wenzel creó Isar (Intelligible semi-automated reasoning). Isar está construido sobre el sistema Isabelle. Isabelle es un asistente de prueba genérico desarrollado por L. Paulson (en la Universidad de Cambridge) y T. Nipkow (en la Universidad Politécnica de Munich). Las teorías formalizadas en Isabelle/Isar se encuentran fundamentalmente en la biblioteca de Isabelle2009-1, en la revista The Archive of Formal Proofs y en la IsarMathLib (A library of formalized mathematics for Isabelle/ZF theorem proving environment).

Por lo que respecta a la certificación computacional del conocimiento
matemático los antecedentes pueden situarse en el 1993 con la publicación del manifiesto del proyecto QED impulsado por Bob Boyer y la revisión del proyecto QED en 2007 por F. Wiedijk. Actualmente se han demostrado muchos teoremas matemáticos importantes, como puede comprobarse en Formalizing 100 Theorems, en la NASA Langley PVS Libraries y en The Coq Users’ Contributions. Entre los teoremas formalmente certificados podemos citar el teorema de de la distribución de los números primos, el teorema de los cuatro colores y el teorema de la curva de Jordan. Nuestro grupo posee experiencia en la certificación de teoremas matemáticos habiendo certificado en ACL2 y PVS, entre otros, el lema de Newman, el teorema de Knuth-Bendix, el teorema de corrección del algoritmo de Buchberger, el teorema de Bezem de completitud de la resolución proposicional y el teorema de completitud de la resolución SLD.

Presentación de sistemas de razonamiento

PorJosé A. Alonso

Esta semana se ha celebrado un curso en la Facultad de Matemáticas sobre Software libre frente a software comercial: posibilidades y aplicaciones a la docencia. Dentro del curso hice una presentación de sistemas de razonamiento automático. En la presentación comento brevemente cómo trabajar con distintos sistemas de razonamiento (Otter/MACE, ACL2, PVS e Isabelle/Isar) usados por nuestro grupo y algunas aplicaciones de los distintos sistemas.

Trabajo del Grupo de Lógica Computacional (1987-2009)

PorJosé A. Alonso

El inicio del primer trabajo sobre la automatización del razonamiento. Los trabajos realizados desde entonces se encuentran en las páginas de publicaciones, tesis y trabajos de investigación dirigidos y cursos impartidos. La ordenación de estas páginas es simplemente cronológica. Una visión más ordenada del trabajo desarrollado durante estos años se encuentra en las transparencias de las conferencias que dí en la Universidad de La Coruña: Un viaje a través del razonamiento automático (Experiencias del GLC de la US). En ella se describen los sistemas de razonamiento que hemos utilizado y las teorías que hemos formalizado.