Diferencia entre revisiones de «Documentación»
De Demostración automática de teoremas (2014-15)
(→Visiones generales) |
(→Visiones generales) |
||
| Línea 2: | Línea 2: | ||
== Visiones generales == | == Visiones generales == | ||
| − | # J. Aransay y C. Domínguez. [http://www.google.es/url?sa=t&rct=j&q=&esrc=s&source=web&cd= | + | # J. Aransay y C. Domínguez. [http://www.google.es/url?sa=t&rct=j&q=&esrc=s&source=web&cd=3&ved=0CDQQFjAC&url=http%3A%2F%2Fgaceta.rsme.es%2Fenglish%2Fabrir.php%3Fid%3D1057&ei=LhHnVJfdOYLpUouwgegP&usg=AFQjCNHY4d4tmBPPhiuyR9H2MZssqvJ1WQ&sig2=F7ubkf22PbeGxRUsFWNCtQ&bvm=bv.86475890,d.d24 Demostración asistida por ordenador]. RSME Volume 15, issue 1 (2012). |
# J. Avigad. [http://www.andrew.cmu.edu/user/avigad/Talks/icerm.pdf Interactive theorem proving, automated reasoning, and mathematical computation]. ICERM, 14 de diciembre de 2012. | # J. Avigad. [http://www.andrew.cmu.edu/user/avigad/Talks/icerm.pdf Interactive theorem proving, automated reasoning, and mathematical computation]. ICERM, 14 de diciembre de 2012. | ||
# J. Harrison. [http://www.cl.cam.ac.uk/~jrh13/papers/ab.html A short survey of automated reasoning]. ''Lecture Notes in Computer Science'', Vol. 4545, pp. 334-349, 2007. | # J. Harrison. [http://www.cl.cam.ac.uk/~jrh13/papers/ab.html A short survey of automated reasoning]. ''Lecture Notes in Computer Science'', Vol. 4545, pp. 334-349, 2007. | ||
Revisión del 12:48 20 feb 2015
En esta página se recogen en enlaces que sirven de documentación al curso de Demostración automática de teoremas (DAT).
Sumario
Visiones generales
- J. Aransay y C. Domínguez. Demostración asistida por ordenador. RSME Volume 15, issue 1 (2012).
- J. Avigad. Interactive theorem proving, automated reasoning, and mathematical computation. ICERM, 14 de diciembre de 2012.
- J. Harrison. A short survey of automated reasoning. Lecture Notes in Computer Science, Vol. 4545, pp. 334-349, 2007.
- J. Harrison. Formal proof: Theory and practice. Notices of the AMS, Vol. 55, N. 11 (2008) p.1395-1406.
Referencias sobre Isabelle/HOL
- T. Nipkow Programming and proving in Isabelle/HOL. 5 de diciembre de 2013.
- T. Nipkow, M. Wenzel y L.C. Paulson A proof assistant for higher-order logic. Springer-Verlag. 5 de diciembre de 2013.
- Isabelle/HOL — Higher-Order Logic. 5 de diciembre de 2013.
- M. Wenzel The Isabelle/Isar Reference Manual. 5 de diciembre de 2013.
- M. Wenzel The Isabelle/Isar quick reference.
- J. Siek Quick Reference for Isabelle/Isar Propositional Logic.
- J. Siek Quick Reference for Isabelle/Isar More Proof Techniques.
- J. Siek Quick Reference for Isabelle/Isar First-Order Logic.
- Tutorials and manuals for Isabelle2013.
Cursos con Isabelle/HOL
- Tobias Nipkow. Semantics of programming languages. (Univ. de Munich, 2012-13).
- Tobias Nipkow Theorem Proving with Isabelle/HOL An Intensive Course.
- Larry Paulson. Interactive Formal Verification. (Univ. de Cambridge, 2009-10).
- Jeremy G. Siek. Theorem proving in Isabelle.(Univ. de Colorado, 2011).
- Tjark Weber. Interactive Formal Verification. (Univ. de Cambridge, 2010-11).
Bibliotecas de ejemplos de verificación
- Archive of Formal Proofs.
- Formalizing 100 Theorems.
- Gallery of verified programs.
- Larry Wos' Notebooks.
- The TPTP Problem Library for Automated Theorem Proving.
- VerifyThis (A collection of verification benchmarks.