Reseña: Inteligencia artificial avanzada

En la colección de textos de la UOC (Universitat Oberta de Catalunya) se ha publicado el libro Inteligencia artificial avanzada.

Sus autores son Raúl Benítez, Gerard Escudero y Samir Kanaan.

El libro está organizado de la forma siguiente: los métodos de búsqueda y optimización se describen en el apartado 2, donde se detallarán las técnicas de extracción de información de bases de datos que contengan información semántica, como por ejemplo web de noticias o las conversaciones entre diversos miembros de una red social.

Las técnicas de caracterización de datos se estudiarán en el apartado 3, describiendo las técnicas principales basadas en descomposición de los datos en modos principales. En el apartado 3 también se estudiarán las técnicas de extracción de características y un método de visualización de datos multidimensionales.

Los algoritmos de clasificación de datos se presentan en el apartado 4, en el que se estudiarán los principales métodos de clasificación y reconocimiento de patrones.

En el apartado 5 se explican algunas técnicas avanzadas de inteligencia evolutiva, algoritmos que utilizan reglas heurísticas inspiradas en el funcionamiento evolutivo de los sistemas biológicos.

El código del texto está escrito en Python. Una introducción a Python se encuentra en otro texto de la UOC: El lenguaje Python escrito por David Masip Rodó– El objetivo del texto es ayudar a comprender los ejemplos que se exponen en el libro de inteligencia artificial.

Ambos libros son la base de la asignatura Intel·ligència artificial avançada impartida por David Masip Rodó en el Màster en Enginyeria Informàtica de la UOC.

Reseña: El uso de los demostradores automáticos de teoremas para la enseñanza de la programación

Se ha publicado un artículo sobre el uso de Krakatoa en la enseñanza titulado El uso de los demostradores automáticos de teoremas para la enseñanza de la programación.

Su autora es Ana Romero (de la Universidad de la Rioja) y lo ha presentado en la Jenui 2013 (XIX Jornadas sobre la Enseñanza Universitaria de la Informática).

Su resumen es

La verificación formal de algoritmos, impartida en los estudios de Ingeniería Informática como parte de las asignaturas de programación, se suele explicar de manera “teórica” introduciendo los axiomas de la lógica de Hoare y realizando diversos ejercicios de verificación (a mano) de pequeños programas. Aunque los alumnos han debido adquirir previamente los conocimientos de Lógica necesarios, muchos de ellos presentan serias dificultades para expresar formalmente los distintos pasos de las pruebas de corrección planteadas. En esta experiencia se ha decidido utilizar como herramienta de apoyo para explicar la verificación formal de algoritmos un demostrador automático de teoremas llamado Krakatoa. Esta herramienta permitirá a los estudiantes visualizar de manera interactiva los distintos pasos necesarios para probar la corrección de un programa, reflexionar sobre los razonamientos seguidos y comprender la importancia de la verificación de algoritmos para mejorar la fiabilidad de nuestros programas.

Reseña: “An intelligent tutoring system for teaching FOL equivalence”

Se ha publicado un artículo sobre enseñanza de la lógica titulado An intelligent tutoring system for teaching FOL equivalence.

Sus autores son Foteini Grivokostopoulou, Isidoros Perikos, Ioannis Hatzilygeroudis (de la Universidad de patras en Grecia).

El trabajo se ha presentado hoy en el AIEDCS 2013 (The First Workshop on AI-supported Education for Computer Science).

Su resumen es

In this paper, we present an intelligent tutoring system developed to assist students in learning logic. The system helps students to learn how to construct equivalent formulas in first order logic (FOL), a basic knowledge representation language. Manipulating logic formulas is a cognitively complex and error prone task for the students to deeply understand. The system assists stu- dents to learn to manipulate and create logically equivalent formulas in a step-based process. During the process the system provides guidance and feedback of various types in an intelligent way based on user’s behavior. Evaluation of the system has shown quite satisfactory results as far as its usability and learning capabilities are concerned.

Reseña: “Computational verification of network programs in Coq”

Se ha publicado un artículo de verificación formal en Coq titulado Computational verification of network programs in Coq.

Su autor es Gordon Stewart (miembro del proyecto Verified Software Toolchain la Universidad de Princeton).

Su resumen es

We report on the design of the first fully automatic, machine-checked tool suite for verification of high-level network programs. The tool suite targets programs written in NetCore, a new declarative network programming language. Our work builds on a recent effort by Guha, Reitblatt, and Foster to build a machine-verified compiler from NetCore to OpenFlow, a new protocol for software-defined networking. The result is an end-to-end system that provides strong guarantees on the compiled OpenFlow flow tables that are installed on actual network switches.

El correspondiente código en Coq se encuentra aquí.

Lecturas del Grupo de Lógica Computacional (Junio de 2013)

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional desde el mes de enero de 2013. La anterior recopilación fue la de diciembre 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.

  1. Problemas sobre el 2013 en Haskell. #Haskell
  2. La sucesión de Perrin en Haskell. #Haskell
  3. Representación de 2ⁿ como 7x²+y² (con x e y impares) en Haskell #Haskell
  4. Computing square roots using the babylonian method. #Isabelle
  5. Formal verification of nonlinear inequalities with Taylor interval approximations. #HOL_Light
  6. Characteristic formulae for mechanized program verification. #Tesis #Coq
  7. Construction and stochastic applications of measure spaces in Higher-Order Logic. #Tesis #Isabelle
  8. A proof of Bertrand’s postulate. #Matita
  9. Trusting computations: a mechanized proof from partial differential equations to actual program. #Coq
  10. Formal construction of a set theory in Coq. #Tesis #Coq
  11. Rank-nullity theorem in linear algebra. #Isabelle #AFP
  12. GDT4MAS: a formal model and language to specify and verify agent-based complex systems. #PVS
  13. Kleene algebra. #AFP #Isabelle
  14. Information-theoretic analysis using theorem proving. #Tesis #HOL4
  15. Applying formal methods in software development. #Tesis #PVS
  16. Formalization and concretization of ordered networks. #Coq
  17. The design of a practical proof checker for a lazy functional language. #MProver #Haskell
  18. The formalization of syntax-based mathematical algorithms using quotation and evaluation
  19. A verified decision procedure for MSO on words based on derivatives of regular expressions. #Isabelle
  20. Statistical proof-patterns in Coq/SSReflect. #Coq
  21. Towards a logic-based unifying framework for computing.
  22. Termination tools in automated reasoning. #Tesis
  23. Matrices à blocs et en forme canonique. #Coq
  24. Automated verification of termination certificates. #Coq
  25. Formalized algebraic numbers: construction and first-order theory. #Tesis #Coq
  26. Towards self-verification of Isabelle’s Sledgehammer. #Isabelle
  27. A framework for the verification of certifying computations. #Isabelle
  28. A preliminary univalent formalization of the p-adic numbers. #Coq
  29. Algunos vínculos entre los teoremas de Gödel y Turing
  30. Formal computations and methods. #Tesis #HOL_Light
  31. Complex concept lattices for simulating human prediction in sport.
  32. MaSh: Machine learning for Sledgehammer. #Isabelle #ITP2013
  33. Une étude formelle de la théorie des calculs locaux à l’aide de l’assistant de preuve Coq. #Tesis #Coq
  34. Temas de programación lógica e inteligencia artificial. #Prolog
  35. Una curiosa propiedad del 123 en Haskell. #Haskell
  36. A report on an experiment in porting formal theories from Isabelle/HOL to Ecore and OCL2. #Isabelle #ACL2
  37. Otra curiosa propiedad del 123 en Haskell. #Haskell
  38. Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos. #PVS
  39. Mechanising Turing machines and computability theory in Isabelle/HOL. #Isabelle
  40. ML4PG: proof-mining in Coq. #Coq
  41. Concept-forming operators on multilattices. #AFC
  42. The gauge integral theory in HOL4. #HOL4
  43. The Picard algorithm for ordinary differential equations in Coq. #Coq
  44. Mechanising Turing machines and computability theory in Isabelle/HOL. #Isabelle #ITP2013
  45. Formal reasoning about finite-state discrete-time Markov chains in HOL. #HOL
  46. Verifying a plaftorm for digital imaging: a multi-tool strategy. #Coq #ACL2
  47. Deducción natural en lógica proposicional con Isabelle/HOL. #Isabelle
  48. Formalized algebraic numbers: construction and first-order theory. #Tesis #Coq
  49. Knowledge representation, reasoning, and the design of intelligent agents. #Libro #ASP
  50. A hierarchy of mathematical structures in ACL2. #ACL2
  51. Programming and reasonning with powerlists in Coq. #Coq
  52. Formalization of the complex number theory in HOL4. #HOL4
  53. Formalizing the confluence of orthogonal rewriting systems. #PVS
  54. Homotopy limits in Coq. #Coq
  55. Data refinement in Isabelle/HOL. #Isabelle_HOL
  56. Formalization of real analysis: A survey of proof assistants and libraries. #ITP
  57. AI over large formal knowledge bases: The first decade. #Mizar
  58. ForMaRE-formal mathematical reasoning in economics.
  59. A fully verified executable LTL model checker. #Isabelle
  60. Automating inductive proofs using theory exploration. #Haskell #HipSpec
  61. One logic to use them all. #CADE24 #Why3
  62. Square root and division elimination in PVS. #PVS #ITP2013
  63. Experience report: Teaching Haskell to the masses. #Haskell
  64. Coinductive pearl: Modular first-order logic completeness. #Isabelle
  65. Formalization of incremental simplex algorithm by stepwise refinement. #Isabelle
  66. Les assistants de preuve, ou comment avoir confiance en ses démonstrations. #DAO
  67. Developing an auction theory toolbox. #Isabelle
  68. Formalizing Knuth-Bendix orders and Knuth-Bendix completion. #Isabelle
  69. A formal proof of Kruskal’s tree theorem in Isabelle/HOL. #Isabelle
  70. A constructive theory of regular languages in Coq. #Coq
  71. A machine-checked proof of the odd order theorem. #Coq
  72. Graph theory. #Isabelle #AFP
  73. A macro for reusing abstract functions and theorems. #ACL2
  74. Light-weight containers for Isabelle: efficient, extensible, nestable. #Isabelle
  75. Formalizing Turing machines. #Matita
  76. A certified reduction strategy for homological image processing. #Coq
  77. On the formalization of continuous-time Markov chains in HOL. #HOL
  78. A Web interface for Isabelle: The next generation. #Isabelle #CICM2013
  79. Verifying refutations with extended resolution. #ACL2
  80. Type classes and filters for mathematical analysis in Isabelle/HOL. #Isabelle
  81. Mechanical verification of SAT refutations with extended resolution. #ACL2 #ITP2013
  82. The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups). #Coq
  83. Automatic data refinement. #Isabelle #ITP2013
  84. Certified HLints with Isabelle/HOLCF-Prelude. #Isabelle
  85. Theorem of three circles in Coq. #Coq
  86. A Haskell library for term rewriting. #Haskell
  87. Formal mathematics on display: A wiki for Flyspeck. #HOL_Light
  88. Solveurs CP(FD) vérifiés formellement. #Coq
  89. Formalizing bounded increase. #Isabelle
  90. Certified symbolic manipulation: Bivariate simplicial polynomials. #ACL2
  91. The formalization of syntax-based mathematical algorithms using quotation and evaluation.
  92. Homotopy type theory: Univalent foundations of mathematics. #Libro
  93. Mathematicians think like machines for perfect proofs.
  94. Certifying homological algorithms to study biomedical images. #Tesis #Coq #Haskell
  95. Formalizing cut elimination of coalgebraic logics in Coq. #Coq

La recopilación de las lecturas anteriores se encuentra aquí.