Demostración automática de teoremas (2014-15) Demostración automática de teoremas (2014-15)

En esta página se recogen en enlaces que sirven de documentación al curso de Demostración automática de teoremas (DAT).

Visiones generales

1. J. Aransay y C. Domínguez. Demostración asistida por ordenador. RSME Volume 15, issue 1 (2012).
2. J. Avigad. Interactive theorem proving, automated reasoning, and mathematical computation. ICERM, 14 de diciembre de 2012.
3. J. Harrison. A short survey of automated reasoning. Lecture Notes in Computer Science, Vol. 4545, pp. 334-349, 2007.
4. J. Harrison. Formal proof: Theory and practice. Notices of the AMS, Vol. 55, N. 11 (2008) p.1395-1406.

Referencias sobre Isabelle/HOL

1. T. Nipkow Programming and proving in Isabelle/HOL. 5 de diciembre de 2013.
2. T. Nipkow, M. Wenzel y L.C. Paulson A proof assistant for higher-order logic. Springer-Verlag. 5 de diciembre de 2013.
3. Isabelle/HOL — Higher-Order Logic. 5 de diciembre de 2013.
4. M. Wenzel The Isabelle/Isar Reference Manual. 5 de diciembre de 2013.
5. M. Wenzel The Isabelle/Isar quick reference.
6. J. Siek Quick Reference for Isabelle/Isar Propositional Logic.
7. J. Siek Quick Reference for Isabelle/Isar More Proof Techniques.
8. J. Siek Quick Reference for Isabelle/Isar First-Order Logic.
9. Tutorials and manuals for Isabelle2013.

Cursos con Isabelle/HOL

1. Tobias Nipkow. Semantics of programming languages. (Univ. de Munich, 2012-13).
2. Tobias Nipkow Theorem Proving with Isabelle/HOL An Intensive Course.
3. Larry Paulson. Interactive Formal Verification. (Univ. de Cambridge, 2009-10).
4. Jeremy G. Siek. Theorem proving in Isabelle.(Univ. de Colorado, 2011).
5. Tjark Weber. Interactive Formal Verification. (Univ. de Cambridge, 2010-11).

Bibliotecas de ejemplos de verificación

1. Archive of Formal Proofs.
2. Formalizing 100 Theorems.
3. Gallery of verified programs.
4. Larry Wos' Notebooks.
5. The TPTP Problem Library for Automated Theorem Proving.
6. VerifyThis (A collection of verification benchmarks.