Diferencia entre revisiones de «Documentación»
De Demostración automática de teoremas (2014-15)
(→Bibliotecas de ejemplos de verificación) |
|||
| Línea 65: | Línea 65: | ||
# [http://verifythis.cost-ic0701.org VerifyThis (A collection of verification benchmarks]. | # [http://verifythis.cost-ic0701.org VerifyThis (A collection of verification benchmarks]. | ||
| + | <!-- | ||
== Artículos recientes == | == Artículos recientes == | ||
# [http://bit.ly/1iZjgqN Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem]. L. Noschinski | # [http://bit.ly/1iZjgqN Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem]. L. Noschinski | ||
| Línea 138: | Línea 139: | ||
# [http://goo.gl/KkU6s A hierarchy of mathematical structures in ACL2]. ~ J. Heras, F.J. Martín y V. Pascual. | # [http://goo.gl/KkU6s A hierarchy of mathematical structures in ACL2]. ~ J. Heras, F.J. Martín y V. Pascual. | ||
# [http://www.inf.kcl.ac.uk/staff/urbanc/Publications/tm.pdf Mechanising Turing Machines and Computability Theory in Isabelle/HOL] ~ J. Xu, X. Zhang y C. Urban | # [http://www.inf.kcl.ac.uk/staff/urbanc/Publications/tm.pdf Mechanising Turing Machines and Computability Theory in Isabelle/HOL] ~ J. Xu, X. Zhang y C. Urban | ||
| + | --> | ||
Revisión del 11:36 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.
- 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.