Lógica computacional y teoría de conjuntos: Aplicación de la lógica formalizada al análisis

Opiniones de los lectores

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

Título original:

Computational Logic and Set Theory: Applying Formalized Logic to Analysis

Contenido del libro:

A medida que los programas informáticos se hacen más complejos, la cuestión de cómo garantizar su corrección se hace cada vez más crítica. La lógica formal incorporada a los programas informáticos es una parte importante de la respuesta a este problema.

Este texto de lectura obligada presenta los trabajos pioneros del difunto profesor Jacob (Jack) T. Schwartz sobre lógica computacional y teoría de conjuntos y su aplicación a las técnicas de verificación de pruebas, que culminaron en el sistema tnaNova, un prototipo de programa informático diseñado para verificar la corrección de las pruebas matemáticas presentadas en el lenguaje de la teoría de conjuntos. Adoptando un enfoque sistemático, el libro comienza con un estudio de las ramas tradicionales de la lógica antes de describir en detalle el diseño subyacente del sistema tnaNova. A continuación, se utiliza este sistema para derivar varios de los principales resultados clásicos sobre indecidibilidad e irresolubilidad. Los lectores no necesitan grandes conocimientos de lógica formal para seguir el texto, aunque se presupone una buena comprensión de las técnicas de programación estándar y una familiaridad con las matemáticas de las definiciones y los escenarios de prueba.

Temas y características: con un Prólogo del Dr. Martin Davis, catedrático emérito del Instituto Courant de Ciencias Matemáticas de la Universidad de Nueva York; describe en profundidad cómo se puede explotar una teoría específica de primer orden para modelar y llevar a cabo razonamientos en ramas de la informática y las matemáticas; presenta un sistema único para la verificación automatizada de pruebas en sistemas de software a gran escala; integra importantes cuestiones de ingeniería de pruebas, reflejando los objetivos de los verificadores a gran escala; incluye un apéndice que muestra pruebas formalizadas de ordinales, de varias propiedades de la operación de cierre transitivo, de principios de inducción finitos y transfinitos, y del lema de Zorn.

Esta obra pionera es una lectura esencial para investigadores y licenciados avanzados en informática.