Acciones

Diferencia entre revisiones de «Documentación»

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

(→‎Cursos con Isabelle/HOL)
 
(No se muestran 9 ediciones intermedias de 2 usuarios)
Línea 2: Línea 2:
  
 
== Visiones generales ==
 
== Visiones generales ==
−
# J. Aransay y C. Domínguez. Demostración asistida por ordenador.
+
# 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.
Línea 11: Línea 11:
 
# T. Nipkow, M. Wenzel y L.C. Paulson [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/doc/tutorial.pdf A proof assistant for higher-order logic]. Springer-Verlag. 5 de diciembre de  2013.
 
# T. Nipkow, M. Wenzel y L.C. Paulson [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/doc/tutorial.pdf A proof assistant for higher-order logic]. Springer-Verlag. 5 de diciembre de  2013.
 
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL/document.pdf Isabelle/HOL — Higher-Order Logic]. 5 de diciembre de 2013.
 
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL/document.pdf Isabelle/HOL — Higher-Order Logic]. 5 de diciembre de 2013.
−
# M. Wenzel [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/doc/isar-ref.pdf The Isabelle/Isar Reference Manual]. 5 de diciembre de 2013.
+
# M. Wenzel [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2014/doc/isar-ref.pdf The Isabelle/Isar Reference Manual].
 
# M. Wenzel [https://www.lri.fr/~wenzel/Isabelle2011-Paris/quickref.pdf The  Isabelle/Isar quick reference].
 
# M. Wenzel [https://www.lri.fr/~wenzel/Isabelle2011-Paris/quickref.pdf The  Isabelle/Isar quick reference].
 
# J. Siek [http://ecee.colorado.edu/~siek/ecen3703/spring10/quick-ref.pdf Quick Reference for Isabelle/Isar Propositional Logic].
 
# J. Siek [http://ecee.colorado.edu/~siek/ecen3703/spring10/quick-ref.pdf Quick Reference for Isabelle/Isar Propositional Logic].
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]).
 +
-->
  
−
-->
+
== Cursos con Isabelle/HOL ==
−
== Cursos relacionados ==
 
−
=== Cursos con Isabelle/HOL ===
 
 
# Tobias Nipkow. [http://www4.informatik.tu-muenchen.de/~nipkow/semantics/ Semantics of programming languages]. (Univ. de Munich, 2012-13).
 
# Tobias Nipkow. [http://www4.informatik.tu-muenchen.de/~nipkow/semantics/ Semantics of programming languages]. (Univ. de Munich, 2012-13).
 
# Tobias Nipkow [http://isabelle.in.tum.de/coursematerial/PSV2009-1 Theorem Proving with Isabelle/HOL An Intensive Course].  
 
# Tobias Nipkow [http://isabelle.in.tum.de/coursematerial/PSV2009-1 Theorem Proving with Isabelle/HOL An Intensive Course].  
Línea 62: Línea 60:
 
# [http://www.cs.ru.nl/~freek/100 Formalizing 100 Theorems].
 
# [http://www.cs.ru.nl/~freek/100 Formalizing 100 Theorems].
 
# [http://toccata.lri.fr/gallery Gallery of verified programs].
 
# [http://toccata.lri.fr/gallery Gallery of verified programs].
−
# [http://www.cs.nott.ac.uk/~lad/research/challenges/ Induction Challenge Problems].
 
 
# [http://automatedreasoning.net/ Larry Wos' Notebooks].
 
# [http://automatedreasoning.net/ Larry Wos' Notebooks].
 
# [http://www.cs.miami.edu/~tptp/ The TPTP Problem Library for Automated Theorem Proving].
 
# [http://www.cs.miami.edu/~tptp/ The TPTP Problem Library for Automated Theorem Proving].
−
# [http://www.macs.hw.ac.uk/vstte10/Competition.html The 1st Verified Software Competition].
 
−
# [https://sites.google.com/site/vstte2012/compet The 2nd Verified Software Competition].
 
 
# [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 142: Línea 138:
 
# [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 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).

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. 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.


Obtenido de «https://www.glc.us.es/~jalonso/DAT2015/index.php?title=Documentación&oldid=44»