Manual de lógica práctica y razonamiento automatizado

Opiniones de los lectores

El libro es muy elogiado por su enfoque exhaustivo y práctico de la demostración automatizada de teoremas (ATP), en particular a través de su detallada implementación en OCaml. Los lectores aprecian la claridad y amenidad de la escritura, aunque hay algunos inconvenientes en cuanto a su uso como referencia.

⬤ Excelente introducción a la demostración automatizada de teoremas con una clara progresión desde lo básico a temas avanzados.
⬤ Implementaciones completas de algoritmos en OCaml, mejorando la claridad y la comprensión.
⬤ Estilo de escritura ameno que hace que el tema sea atractivo.
⬤ Adecuado para construir su propio demostrador de teoremas automatizado desde cero.
⬤ Considerado imprescindible para los interesados en procedimientos de decisión automatizados.

⬤ Cobertura limitada de solucionadores SMT modernos.
⬤ El uso de OCaml puede ser visto como una desventaja en comparación con lenguajes más utilizados como C++ o Java.
⬤ Puede llevar mucho tiempo buscar implementaciones de funciones básicas cuando se utiliza el libro como referencia y no como tutorial.

(basado en 5 opiniones de lectores)

Título original:

Handbook of Practical Logic and Automated Reasoning

Contenido del libro:

Este libro responde a la demanda de una exposición autocontenida y amplia de los conceptos, la maquinaria y el uso del razonamiento automatizado.

Los fundamentos de la lógica matemática se describen junto con la aplicación práctica, todo ello con un mínimo de requisitos previos. El enfoque es constructivo, concreto y algorítmico: una característica clave es que los métodos se describen con referencia a implementaciones reales (para las que se suministra código) que los lectores pueden utilizar, modificar y con las que pueden experimentar.

Este libro es ideal para quienes busquen una fuente única en el ámbito general del razonamiento automatizado. Puede utilizarse como referencia o para aprender los fundamentos, ya sea en combinación con cursos avanzados o para el autoaprendizaje.