Diferencia entre revisiones de «Documentación»
De Demostración automática de teoremas (2014-15)
(→Referencias sobre Isabelle/HOL) |
|||
| (No se muestra una edición intermedia del mismo usuario) | |||
| Línea 17: | Línea 17: | ||
# J. Siek [http://ecee.colorado.edu/~siek/ecen3703/spring10/quick-ref3.pdf Quick Reference for Isabelle/Isar First-Order Logic]. | # J. Siek [http://ecee.colorado.edu/~siek/ecen3703/spring10/quick-ref3.pdf Quick Reference for Isabelle/Isar First-Order Logic]. | ||
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/documentation.html Tutorials and manuals for Isabelle2013]. | # [http://www.cl.cam.ac.uk/research/hvg/Isabelle/documentation.html Tutorials and manuals for Isabelle2013]. | ||
| − | |||
<!-- | <!-- | ||
== Lecturas complementarias == | == Lecturas complementarias == | ||
| Línea 30: | Línea 29: | ||
# K. Doets y J. van Eijck [http://www.ldc.usb.ve/~astorga/Haskell.Road.pdf The Haskell Road to Logic, Maths and Programming]. | # K. Doets y J. van Eijck [http://www.ldc.usb.ve/~astorga/Haskell.Road.pdf The Haskell Road to Logic, Maths and Programming]. | ||
# M. Huth y M. Ryan [http://goo.gl/TMqOo Logic in computer science: Modelling and reasoning about systems]. Cambridge University Press, 2004. (Incluye el [http://www.cs.bham.ac.uk/research/lics/tutor/index.html tutor en la Red]). | # M. Huth y M. Ryan [http://goo.gl/TMqOo Logic in computer science: Modelling and reasoning about systems]. Cambridge University Press, 2004. (Incluye el [http://www.cs.bham.ac.uk/research/lics/tutor/index.html tutor en la Red]). | ||
| − | |||
--> | --> | ||
Revisión actual del 13:59 3 mar 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.
- 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.