Estoy buscando un libro introductorio sobre lógica matemática que también analice una implementación de su lógica en un asistente de prueba. Me parece que esta sería una excelente manera de aprender lógica matemática, ya que muchos conceptos se volverían muy claros y concretos cuando se implementaran en un programa de computadora. Pero nunca he visto un libro así.
Preferiblemente, el libro introduciría el lenguaje del asistente de prueba sin tener conocimientos previos y animaría al lector a utilizarlo en varios puntos.
EDITAR
Me gustan las respuestas publicadas hasta ahora y quiero mantener esto abierto por un tiempo para recopilar otras recomendaciones en un solo lugar. Sin embargo, después de abrirlo, también encontré los siguientes recursos excelentes vinculados en esta pregunta, a saber, esta lista de recursos y este libro/compilación de notas de Jeremy Avigad. Estos recursos parecen ser el tipo de cosas que estaba buscando y podrían ser útiles para otras personas que encuentren esta publicación.
EDITAR 2
Una característica que realmente me gustaría ver, que no he visto en las sugerencias hasta ahora, es un libro que también formalice su meta-lógica dentro de un asistente de prueba. Por ejemplo, me encantaría un libro que demuestre (por ejemplo) un teorema de solidez y muestre cómo se podría implementar dicha prueba con un asistente de prueba.
Por otra parte, me sorprendería si existiera tal recurso, ya que ningún libro de lógica matemática (que haya visto) menciona siquiera la idea de formalizar la meta-lógica.
Recomiendo encarecidamente el Manual de lógica práctica y razonamiento automatizado de John Harrison . Los ejemplos de programación tienen más que ver con cómo implementar asistentes de prueba y procedimientos de decisión que con cómo usar un asistente de prueba, pero creo que satisfacen su deseo de implementaciones que aclaren los conceptos clave. Todos los ejemplos se dan en el lenguaje de programación funcional OCaml .
Con respecto a la segunda edición: creo que está implícito en la mayoría de los textos sobre lógica matemática que el tema se puede formalizar en un sistema de base adecuado como ZF. En la literatura de lógica matemática esto se vuelve importante y se hace explícito en el trabajo sobre la independencia . En el mundo de los asistentes de prueba, la autoformalización con vistas a una mayor seguridad y comprensión ha sido de interés durante muchos años. Por ejemplo, consulte este documento sobre la autoverificación de HOL y las referencias que contiene. Creo que los principios generales de una metalógica formalizada son probablemente más instructivos que los detalles finos de la formalización.
Pruebe métodos de prueba fundamentales en informática. Utiliza Athena como asistente de prueba. Enseña tanto la lógica como el lenguaje.
Si encuentra ese complejo aquí, uno simple: https://staff.washington.edu/jon/flip/www/userguide-nd.html Funciona con Python 2.7.
Los libros que tienen un asistente de prueba que lo acompaña para su lógica es una forma de verlo, pero también funciona al revés: la mayoría de los asistentes de prueba implementan alguna lógica particular (generalmente constructiva) y, por lo tanto, los libros sobre el asistente de prueba ya son libros sobre esta lógica. .
Aquí hay algunos recursos sobre Coq :
Sofware Foundations Series [Pierce] En particular, el libro 1 introduce la lógica constructiva dentro de Coq.
Modelado y demostración en la teoría de tipos computacional usando Coq [Smolka] es un borrador de un libro en evolución, que es la base de una conferencia y tiene archivos Coq adjuntos en github . Está hablando del asistente de prueba de una manera menos directa.
El sitio de la Comunidad Lean tiene una página sobre recursos de aprendizaje recomendados .
Y no olvidemos las cosas de HoTT:
Daniel Schepler
WillG
Dan Christensen
Léreau
usuario21820
Chico codificador