Procedimientos de decisión: Un punto de vista algorítmico

Opiniones de los lectores

Actualmente no hay opiniones de lectores. La calificación se basa en 12 votos.

Título original:

Decision Procedures: An Algorithmic Point of View

Contenido del libro:

Un procedimiento de decisión es un algoritmo que, dado un problema de decisión, termina con una respuesta correcta sí/no. Aquí, los autores se centran en teorías que son lo suficientemente expresivas como para modelar problemas reales, pero que siguen siendo decidibles.

En concreto, el libro se centra en procedimientos de decisión para teorías de primer orden que se utilizan habitualmente en la verificación y el razonamiento automatizados, la comprobación de teoremas, la optimización de compiladores y la investigación operativa. Las técnicas descritas en el libro proceden de campos como la teoría de grafos y la lógica, y se utilizan habitualmente en la industria. Los autores introducen la terminología básica de las teorías del módulo de la satisfacibilidad y, a continuación, en capítulos separados, estudian los procedimientos de decisión para cada una de las siguientes teorías: lógica proposicional igualdades y funciones no interpretadas aritmética lineal vectores de bits matrices lógica de punteros y fórmulas cuantificadas.

También estudian el problema de la decisión de teorías combinadas y dedican un capítulo a las técnicas modernas basadas en la interacción entre un solucionador SAT y un procedimiento de decisión para la teoría investigada. Este libro de texto se ha utilizado para impartir cursos de licenciatura y posgrado en la ETH de Zúrich, en el Technion de Haifa y en la Universidad de Oxford.

Cada capítulo incluye una bibliografía detallada y ejercicios. En el sitio web de los autores hay disponibles diapositivas para los profesores y una biblioteca en C++ para la creación rápida de prototipos de procedimientos de decisión.