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

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.

I1M2011: Introducción a la programación con Haskell

En la clase de hoy del curso Informática (de 1º de Grado en Matemáticas) se ha presentado una introducción a la programación con Haskell usando emacs como entorno de programación. Concretamente, su objetivo del tema ha sido aprender a:

  • usar Haskell como calculadora aritmética (con las funciones +, -, *, /, div y ^).
  • usar Haskell como calculadora de listas (con las funciones head, tail, take, drop, length, sum, product, ++ y reverse).
  • escribir guiones de Haskell en emacs.
  • cargar los guiones y evaluar expresiones con las funciones definidas.

Como tarea para la próxima clase se ha propuesto instalar GHC y emacs (cuyos enlaces se encuentran en la página de sistemas y escribir de manera colaborativa las soluciones de los ejercicios de la 1º relación.

Las transparencias usadas en la clase son las del tema 2:
Read More “I1M2011: Introducción a la programación con Haskell”

LI2011-12: De la semántica a la deducción natural en lógica proposicional

En la clase de hoy del curso Lógica Informática se ha concluido el estudio de la semántica de la lógica proposicional y se ha empezado el estudio de la deducción natural en lógica proposicional.

De la semántica de la lógica proposicional se ha demostrado la equivalencia entre los distintos problemas semánticos:

  1. decidir si una fórmula es consecuencia lógica de un conjunto finito de as,
  2. decidir si una fórmula es una tautología,
  3. decidir si una fórmula es insatisfacible y
  4. decidir si un conjunto de fórmulas es inconsistente.

También se ha mostrado cómo usar el sistema Gateway to Logic para resolver problemas, aplicándolo al rompecabeza de los veraces y mentirosos. Finalmente, se ha comentado la relación de tipos de problemas.

Teminado el estudio semántico (cuyo problema fundamental es dado un conjunto de fórmulas S y una fórmula F, decidir si F es consecuencia de S (en notación, S |= F)), comenzamos el estudio de los cálculos deductivos (cuyo problema fundamental es dado un conjunto de fórmulas S y una fórmula F, decidir si F es deducible de S (en notación, S |- F)). Además, se requiere que los cálculos sean adecuados y completos (es decir; que S |= F si, y sólo si, S |- F).

El primer cálculo deductivo que estudiamos es el de deducción natural. Las reglas que se han visto en la clase de hoy son las de la conjunción, de la doble negación, de eliminación del condicional, de modus tollens, de introducción del condicional y las de la disyunción.

Como tarea pendiente se propone la resolución de los 36 primeros apartados del ejercicio 5 del tema 2 del libro de ejercicios, cuyas soluciones se encuentran en libro de ejercicios de deducción natural en lógica proposicional.

Las transparencias de esta clase son las páginas 1-12 del tema 2
Read More “LI2011-12: De la semántica a la deducción natural en lógica proposicional”