Algunos comentarios sobre el libro "Decision Procedures"

En un principio, al leer el título de este libro, supuse que sería acerca del procedimiento necesario para la toma de decisiones desde una perspectiva cognitiva, como en el contexto de avatares o agentes o similares. Sin embargo, al comenzar a leerlo, me quedó claro que el tema principal es el razonamiento lógico, la lógica matemática. De cualquier manera, seguí leyendo el material ya que fue refrescante recordar una buena parte de este material ya que aprendí esos tópicos hace algunos años. Me parece que es importante mantener en mente este tipo de contenido para tener la capacidad de formalizar el razonamiento que uno hace cuando está escribiendo de manera científica, y ser capaz de mostrar un mecanismo sólido y completo de porqué llegamos a las conclusiones de lo que decimos.

Siendo más específico, el libro trata los algoritmos necesarios para poder decidir (determinar si una fórmula lógica es válida o no) en diferentes lógicas. Las lógicas que abarca este libro son: lógica proposicional, lógica de equidad y funciones no interpretadas, aritmética linear, vectores de bits, arreglos, lógica de apuntadores, fórmulas cuantificadas, combinación de teorías, y codificación proposicional. Para cada una de ellas, explica brevemente los alcances y las limitaciones sobre las que trabajará, y después algún algoritmo (de varios posibles) para poder decidir, de manera algorítmica, sobre ella.

Por el listado de temas, el lector especializado se podrá dar cuenta que va incrementando la complejidad de las lógicas, pero se aproxima hacia la computabilidad genérica, sin llegar a ella, ya que no es posible. Y las explicaciones que va dando, me parece, tienen una buena didáctica que te hace desear saber más, intentar aplicar los conocimientos adquiridos a tus proyectos personales. Eso me hace recomendar este libro para aquellos interesados en poder formalizar algunas partes de sus proyectos científicos, y después poder crear programas de cómputo para automatizar los procedimientos necesarios.

Sobre este último punto, la automatización, obviamente el libro también menciona, y abarca, el tema de los SAT solvers, incluso explica un poco de la teoría que existe detrás de ellos. Aún más, pone a disposición ciertos programas y códigos (ver el sitio web del libro y el sitio acerca de SMT-Lib) que permiten realizar pruebas sobre un marco de trabajo DPLL (Davis-Putnam-Loveland-Logemann). Esto le podría interesar a aquellos que quieren ver en funcionamiento un programa para verificación automática.

En conclusión, recomendaría este libro, pero no para el público en general, sino para el científico que ya ha tenido un primer acercamiento a la lógica matemática, y que desea conocer más, de una manera amena, acerca de los procedimientos automáticos-algorítmicos que se pueden utilizar para determinar si fórmulas especificadas en alguna lógica en particular son válidas o no.

Referencia bibliográfica:
Decision Procedures - An Algorithmic Point of View
Serie: EATCS Texts in Theoretical Computer Science
Autores: Daniel Kroening, Ofer Strichman
ISBN: 978-3-540-74104-6
DOI: 10.1007/s10817-013-9295-4