Acciones

Diferencia entre revisiones de «Documentación»

De Razonamiento automático (2017-18)

(→‎Visiones generales de la DAO)
 
(No se muestran 4 ediciones intermedias de 2 usuarios)
Línea 1: Línea 1:
−
En esta página se recogen en enlaces que sirven de documentación al curso de "Razonamiento automático"
+
En esta página se recogen en enlaces que sirven de documentación al curso de demostración asistida por ordenador (DAO). Los enlaces están actualizados en el [https://www.glc.us.es/~jalonso/RA2019/index.php/Documentaci%C3%B3n curso 2019-20].
  
 
== Visiones generales de la DAO ==
 
== Visiones generales de la DAO ==
Línea 8: Línea 8:
 
# J.P. Delahaye [http://interstices.info/jcms/int_63417/du-reve-a-la-realite-des-preuves Du rêve à la réalité des preuves]. ''Interstices'', 8 de julio de 2012.
 
# J.P. Delahaye [http://interstices.info/jcms/int_63417/du-reve-a-la-realite-des-preuves Du rêve à la réalité des preuves]. ''Interstices'', 8 de julio de 2012.
 
# J. Germoni [http://images.math.cnrs.fr/Coq-et-caracteres.html Coq et caractères: Preuve formelle du théorème de Feit et Thompson]. ''Images des Mathématiques'', CNRS, 23 de noviembre de 2012.  
 
# J. Germoni [http://images.math.cnrs.fr/Coq-et-caracteres.html Coq et caractères: Preuve formelle du théorème de Feit et Thompson]. ''Images des Mathématiques'', CNRS, 23 de noviembre de 2012.  
−
# H. Geuvers [http://www.ias.ac.in/article/fulltext/sadh/034/01/0003-0025 Proof assistants: History, ideas and future]. ''Sadhana'', Vol. 34-1, pp. 3-25, février 2009.
+
# H. Geuvers [http://www.ias.ac.in/sadhana/Pdf2009Feb/3.pdf Proof assistants: History, ideas and future]. ''Sadhana'', Vol. 34-1, pp. 3-25, février 2009.
 
# G. Gonthier [http://www.ams.org/notices/200811/tx081101382p.pdf The four-color theorem]. ''Notices of the AMS'', Vol. 55, n° 11, pp. 1382-1393, 2008.
 
# G. Gonthier [http://www.ams.org/notices/200811/tx081101382p.pdf The four-color theorem]. ''Notices of the AMS'', Vol. 55, n° 11, pp. 1382-1393, 2008.
−
# Gross, J [https://blogs.ams.org/mathgradblog/2017/10/15/machine-checked-proof Machine-checked proof]. ''AMS Notices', 15 de octubre de 2017.
 
 
# T. Hales. [http://www.ams.org/notices/200811/tx081101370p.pdf Formal proof]. ''Notices of AMS'', Vol. 55, N. 11 (2008) pp. 1370-1380.
 
# T. Hales. [http://www.ams.org/notices/200811/tx081101370p.pdf Formal proof]. ''Notices of AMS'', Vol. 55, N. 11 (2008) pp. 1370-1380.
 
# 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.
 
# J. Harrison. [http://www.ams.org/notices/200811/tx081101395p.pdf Formal proof: Theory and practice]. ''Notices of the AMS'', Vol. 55, N. 11 (2008) p.1395-1406.  
 
# J. Harrison. [http://www.ams.org/notices/200811/tx081101395p.pdf Formal proof: Theory and practice]. ''Notices of the AMS'', Vol. 55, N. 11 (2008) p.1395-1406.  
 
# G. Kolata. [http://www.nytimes.com/library/cyber/week/1210math.html Computer math proof shows reasoning power]. ''The New York Times'', 10 de diciembre de 1996.
 
# G. Kolata. [http://www.nytimes.com/library/cyber/week/1210math.html Computer math proof shows reasoning power]. ''The New York Times'', 10 de diciembre de 1996.
−
# D. MacKenzie [http://www.bcs.org/server.php?show=ConWebDoc.4364 Computers and the sociology of mathematical proof].
+
# D. MacKenzie [https://backspaces.net/temp/Spring2010Seminar/18%20unconventional%20essays%20on%20the%20nature%20of%20mathematics.pdf#page=147 Computers and the sociology of mathematical proof].
−
# G. Sutcliffe. [http://www.cs.miami.edu/~tptp/OverviewOfATP.html What is automated theorem proving?].
+
# G. Sutcliffe. [http://tptp.org/OverviewOfATP.html What is automated theorem proving?].
 
# F. Wiedijk [http://www.cs.ru.nl/~freek/100/ Formalizing the «top 100» of mathematical theorems].
 
# F. Wiedijk [http://www.cs.ru.nl/~freek/100/ Formalizing the «top 100» of mathematical theorems].
 
# F. Wiedijk [http://www.ams.org/notices/200811/tx081101408p.pdf Formal proof - Getting started]. ''Notices of the AMS'', Vol. 55, n° 11, pp. 1408-1414, 2008.
 
# F. Wiedijk [http://www.ams.org/notices/200811/tx081101408p.pdf Formal proof - Getting started]. ''Notices of the AMS'', Vol. 55, n° 11, pp. 1408-1414, 2008.
−
# F. Wiedijk, [http://mizar.org/trybulec65/8.pdf The QED manifesto revisited]. ''Studies in Logic, Grammar and Rhetoric'', Vol. 10(23), pp. 121-133, 2007.
+
# F. Wiedijk, [https://www.cs.ru.nl/F.Wiedijk/pubs/qed2.pdf The QED manifesto revisited]. ''Studies in Logic, Grammar and Rhetoric'', Vol. 10(23), pp. 121-133, 2007.
  
 
== Referencias sobre Isabelle/HOL ==
 
== Referencias sobre Isabelle/HOL ==
−
# B. Grechuk [http://dream.inf.ed.ac.uk/projects/isabelle/Isabelle_Primer.pdf Isabelle primer for mathematicians].
+
# B. Grechuk [https://web.cs.wpi.edu/~dd/resources_isabelle/isabelle_primer_mathematicians.pdf Isabelle primer for mathematicians].
 
# T. Nipkow [https://isabelle.in.tum.de/doc/prog-prove.pdf Programming and proving in Isabelle/HOL].  
 
# T. Nipkow [https://isabelle.in.tum.de/doc/prog-prove.pdf Programming and proving in Isabelle/HOL].  
−
# T. Nipkow, M. Wenzel y L.C. Paulson [http://isabelle.in.tum.de/doc/tutorial.pdf A proof assistant for higher-order logic].
+
# T. Nipkow, M. Wenzel y L.C. Paulson [https://isabelle.in.tum.de/website-Isabelle2009/dist/Isabelle/doc/tutorial.pdf A proof assistant for higher-order logic].  
 
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL/document.pdf Isabelle/HOL — Higher-Order Logic].  
 
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL/document.pdf Isabelle/HOL — Higher-Order Logic].  
−
# M. Wenzel [http://isabelle.in.tum.de/doc/isar-ref.pdf The Isabelle/Isar Reference Manual].
 
−
# M. Wenzel [http://typessummerschool07.cs.unibo.it/courses/wenzel-isar-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-ref2.pdf Quick Reference for Isabelle/Isar More Proof Techniques].
 
−
# 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 Isabelle].
 
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/documentation.html Tutorials and manuals for Isabelle].
  
 
== Lecturas complementarias ==
 
== Lecturas complementarias ==
 
=== Programación funcional ===
 
=== Programación funcional ===
−
# J.A. Alonso [https://www.cs.us.es/~jalonso/cursos/i1m-16/temas/2016-17-IM-temas-PF.pdf  Temas de "Programación funcional"]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2016.
+
# J.A. Alonso [http://www.cs.us.es/~jalonso/cursos/i1m-12/temas/2012-13-IM-temas-PF.pdf  Temas de "Programación funcional"]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
 
# J.A. Alonso y M.J. Hidalgo [http://www.cs.us.es/~jalonso/publicaciones/Piensa_en_Haskell.pdf Piensa en Haskell (Ejercicios de programación funcional con Haskell)]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
 
# J.A. Alonso y M.J. Hidalgo [http://www.cs.us.es/~jalonso/publicaciones/Piensa_en_Haskell.pdf Piensa en Haskell (Ejercicios de programación funcional con Haskell)]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
 
# G. Hutton [http://goo.gl/pKqG Programming in Haskell]. Cambridge University Press, 2007.  
 
# G. Hutton [http://goo.gl/pKqG Programming in Haskell]. Cambridge University Press, 2007.  
Línea 41: Línea 35:
  
 
=== Lógica computacional ===
 
=== Lógica computacional ===
−
# J.A. Alonso [https://www.cs.us.es/~jalonso/cursos/li-15/temas/temas-LI-2015-16.pdf Temas de "Lógica informática" (2015-16)]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2015.
+
# J.A. Alonso [http://www.cs.us.es/~jalonso/cursos/li-12/temas/temas-LI-2012-13.pdf Temas de "Lógica informática" (2012-13)]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
−
# K. Broda, S. Eisenbach, H. Khoshnevisan y S. Vickers [http://pubs.doc.ic.ac.uk/reasoned-programming/reasoned-programming.pdf Reasoned programming]. Imperial College, 1994.
+
# R. Bornat [http://bit.ly/oithic Proof and disproof in formal logic: an introduction for programmers]. Oxford University Press, 2005.
−
# K. Doets y J. van Eijck [http://www.ldc.usb.ve/~astorga/Haskell.Road.pdf The Haskell Road to Logic, Maths and Programming].
+
# K. Broda, S. Eisenbach, H. Khoshnevisan y S. Vickers [https://www.doc.ic.ac.uk/~susan/firstyearbook.pdf Reasoned programming]. Imperial College, 1994.
−
# M. Huth y M. Ryan [http://bit.ly/2e8dFEm 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]).
+
# K. Doets y J. van Eijck [https://books.google.es/books?id=YCC6lwEACAAJ&dq=The+Haskell+Road+to+Logic,+Maths+and+Programming&hl=es&sa=X&redir_esc=y 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]).
  
 
== Cursos relacionados ==
 
== Cursos relacionados ==
 
=== Cursos con Isabelle/HOL ===
 
=== Cursos con Isabelle/HOL ===
−
# Jeremy Avigad. [http://www.phil.cmu.edu/~avigad/formal/ Logic and Formal Verification]. (Carnegie Mellon, 2009).
 
 
# Clemens Ballarin. [http://cl-informatik.uibk.ac.at/teaching/ss08/atp/introduction.php Automatic Deduction]. (Univ de Innsbruck, 2008).
 
# Clemens Ballarin. [http://cl-informatik.uibk.ac.at/teaching/ss08/atp/introduction.php Automatic Deduction]. (Univ de Innsbruck, 2008).
−
# Clemens Ballarin. [http://www4.in.tum.de/~ballarin/belgrade08-tut/ Introduction to the Isabelle Proof Assistant]. (Belgrado, 2008).
 
 
# Clemens Ballarin y Gerwin Klein [http://isabelle.in.tum.de/coursematerial/IJCAR04 Introduction to the Isabelle Proof Assistant]. (en el IJCAR-2004).
 
# Clemens Ballarin y Gerwin Klein [http://isabelle.in.tum.de/coursematerial/IJCAR04 Introduction to the Isabelle Proof Assistant]. (en el IJCAR-2004).
 
# Clemens Ballarin y Tjark Weber. [http://cl-informatik.uibk.ac.at/teaching/ws06/atp/introduction.php Automated Theorem Proving in Isabelle/HOL]. (Univ. de Innsbruck, 2006-07).
 
# Clemens Ballarin y Tjark Weber. [http://cl-informatik.uibk.ac.at/teaching/ws06/atp/introduction.php Automated Theorem Proving in Isabelle/HOL]. (Univ. de Innsbruck, 2006-07).
−
# Jasmin Blanchette, Mathias Fleury y Daniel Wand [http://people.mpi-inf.mpg.de/~jblanche/cswi/ss2015/ Concrete semantics with Isabelle/HOL]. (Univ. del Sarre, 2015-16).
 
 
# A.D. Brucker, D. Basin, J.G. Smaus y B. Wolff. [http://archiv.infsec.ethz.ch/education/permanent/csmr.html Computer-supported Modeling and Reasoning]. (ETH Zurich, 2011).
 
# A.D. Brucker, D. Basin, J.G. Smaus y B. Wolff. [http://archiv.infsec.ethz.ch/education/permanent/csmr.html Computer-supported Modeling and Reasoning]. (ETH Zurich, 2011).
 
# Mads Dam. [http://www.csc.kth.se/utbildning/kth/kurser/DD2453/aform07/ Advanced formal methods]. (KTH Royal Institute of Technology, 2007).
 
# Mads Dam. [http://www.csc.kth.se/utbildning/kth/kurser/DD2453/aform07/ Advanced formal methods]. (KTH Royal Institute of Technology, 2007).
−
# Jacques Fleuriot. [http://www.inf.ed.ac.uk/teaching/courses/ar Automated reasoning]. (Univ. de Edimburgo, 2016-17).
+
# Jacques Fleuriot y Paul Jackson. [http://www.inf.ed.ac.uk/teaching/courses/ar/slides/ Automated reasoning]. (Univ. de Edimburgo, 2012-13).
 
# Thomas Genet [http://www.irisa.fr/celtique/genet/ACF Software formal analysis and design]. (Univ. de Rennes)
 
# Thomas Genet [http://www.irisa.fr/celtique/genet/ACF Software formal analysis and design]. (Univ. de Rennes)
 
# Gerwin Klein. [http://www.cse.unsw.edu.au/~kleing/teaching/thprv-04 Theorem Proving - Principles, Techniques, Applications]. (NICTA, 2004).
 
# Gerwin Klein. [http://www.cse.unsw.edu.au/~kleing/teaching/thprv-04 Theorem Proving - Principles, Techniques, Applications]. (NICTA, 2004).
 
# Gerwin Klein. [http://www.cse.unsw.edu.au/~cs4161/index.html Advanced Topics in Software Verification]. (NICTA, 2012).
 
# Gerwin Klein. [http://www.cse.unsw.edu.au/~cs4161/index.html Advanced Topics in Software Verification]. (NICTA, 2012).
 
# Joao Marcos. [http://www.dimap.ufrn.br/~jmarcos/courses/LC/Ementa.htm Lógica computacional: Demonstração assistida e semi-automática de teoremas].(UFRN, 2000).
 
# Joao Marcos. [http://www.dimap.ufrn.br/~jmarcos/courses/LC/Ementa.htm Lógica computacional: Demonstração assistida e semi-automática de teoremas].(UFRN, 2000).
−
# Tobias Nipkow. [http://www21.in.tum.de/teaching/semantik/WS1617/ Semantics of programming languages]. (Univ. de Munich, 2012-13).
+
# Tobias Nipkow. [https://www21.in.tum.de/teaching/semantics/WS1920/ 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].  
 
# Larry Paulson. [http://www.cl.cam.ac.uk/teaching/0910/L21/ Interactive Formal Verification]. (Univ. de Cambridge, 2009-10).
 
# Larry Paulson. [http://www.cl.cam.ac.uk/teaching/0910/L21/ Interactive Formal Verification]. (Univ. de Cambridge, 2009-10).
−
# Arnd Poetzsch-Heffter. [https://softech.informatik.uni-kl.de/homepage/de/teaching/SVHOL14/ Specification and Verification with Higher-Order Logic].
 
−
# Jeremy G. Siek. [http://www.cs.colorado.edu/~siek/7000/spring07/ Practical Theorem Proving with Isabelle/Isar]. (Univ. de Colorado, 2007).
 
−
# Jeremy G. Siek. [http://ecee.colorado.edu/~siek/ecen5013/spring11/ Theorem proving in Isabelle]. (Univ. de Colorado, 2011).
 
 
# Jan-Georg Smaus. [http://www.informatik.uni-freiburg.de/~ki/teaching/ws0910/csmr/lecture.html Computer-supported modeling and reasoning]. (Univ. de Feiburgo, 2009).
 
# Jan-Georg Smaus. [http://www.informatik.uni-freiburg.de/~ki/teaching/ws0910/csmr/lecture.html Computer-supported modeling and reasoning]. (Univ. de Feiburgo, 2009).
 
# Christian Sternagel [http://cl-informatik.uibk.ac.at/teaching/ss11/eve/content.php Experiments in Verification – Introduction to Isabelle/HOL]. (Univ. de Innsbruck, 2011-12).
 
# Christian Sternagel [http://cl-informatik.uibk.ac.at/teaching/ss11/eve/content.php Experiments in Verification – Introduction to Isabelle/HOL]. (Univ. de Innsbruck, 2011-12).
Línea 72: Línea 61:
  
 
=== Otros cursos ===
 
=== Otros cursos ===
−
# José A. Alonso [http://www.cs.us.es/~jalonso/cursos/li/ Lógica informática] (Univ. de Sevilla, 2012-13).
+
# José A. Alonso [http://www.cs.us.es/~jalonso/cursos/li-12/ Lógica informática] (Univ. de Sevilla, 2012-13).
−
# Thorsten Altenkirch y Peter Morris [http://www.cs.nott.ac.uk/~txa/g52ifr Introduction to formal reasoning] (Univ. de Nottingham, 2010-11).
 
 
# Yves Bertot, Pierre Casteran, Benjamin Gregoire, Pierre Letouzey y Assia Mahboubi [http://www.di.ens.fr/~zappa/teaching/coq/ecole11 Modelling and verifying algorithms in Coq: an introduction]. (INRIA Paris-Rocquencourt, 14-18 noviembre 2011).
 
# Yves Bertot, Pierre Casteran, Benjamin Gregoire, Pierre Letouzey y Assia Mahboubi [http://www.di.ens.fr/~zappa/teaching/coq/ecole11 Modelling and verifying algorithms in Coq: an introduction]. (INRIA Paris-Rocquencourt, 14-18 noviembre 2011).
 
# Pierre Castéran [http://www.labri.fr/perso/casteran/FM/Logique/index.html Logic (Master In Verification)] (Univ. de Burdeos, 2011-12).
 
# Pierre Castéran [http://www.labri.fr/perso/casteran/FM/Logique/index.html Logic (Master In Verification)] (Univ. de Burdeos, 2011-12).
−
# Adam Chlipala [http://stellar.mit.edu/S/course/6/fa11/6.892/ Interactive computer theorem proving]. (MIT, 2012-13).
 
−
# Adam Chlipala y Armando Solar Lezama [https://stellar.mit.edu/S/course/6/fa13/6.820/index.html Foundations of program analysis]. (MIT, 2013-14).
 
−
# Robby Findler [http://www.eecs.northwestern.edu/~robby/courses/395-495-2013-fall Certified programming with dependent types]. (Northwestern, 2013-14).
 
−
# Carlos Luna y Gustavo Betarte. [https://eva.fing.edu.uy/course/view.php?id=363 Construcción formal de programas en teoría de tipos]. (Univ. de la República, Uruguay, 2013-14).
 
 
# Ian Hodkinson [http://www.doc.ic.ac.uk/~imh/teaching/140_logic/logic.html Logic] (Imperial College, Londres, 2010-11).
 
# Ian Hodkinson [http://www.doc.ic.ac.uk/~imh/teaching/140_logic/logic.html Logic] (Imperial College, Londres, 2010-11).
 
# Peter Lucas [http://www.cs.ru.nl/~peterl/teaching/KeR/ Knowledge Representation and Reasoning] (Radboud University # egen, 2011-12).
 
# Peter Lucas [http://www.cs.ru.nl/~peterl/teaching/KeR/ Knowledge Representation and Reasoning] (Radboud University # egen, 2011-12).
 
# Larry Paulson [http://www.cl.cam.ac.uk/Teaching/current/LogicProof/ Logic and Proof] (Univ. de Cambridge, 2011-12).
 
# Larry Paulson [http://www.cl.cam.ac.uk/Teaching/current/LogicProof/ Logic and Proof] (Univ. de Cambridge, 2011-12).
−
# David Pichardie [http://www.irisa.fr/celtique/pichardie/teaching/M2/MDV/ Méthode de vérification] (Universidad de Rennes, 2006-07).
+
# Riccardo Pucella [http://www.ccs.neu.edu/home/riccardo/courses/csu290-sp09/index.html Logic and Computation] (Northeastern University, 2009). Curso con ACL2.
  
 
== Bibliotecas de ejemplos de verificación ==
 
== Bibliotecas de ejemplos de verificación ==
Línea 89: Línea 73:
 
# [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://automatedreasoning.net/ Larry Wos' Notebooks].
 
−
# [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].
 
−
 
−
== Artículos recientes ==
 
−
Están en orden cronológico inverso a la fecha de su reseña en [http://www.glc.us.es/~jalonso/vestigium/tag/resena Vestigium]:
 
−
# [http://bit.ly/1iZjgqN Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem]. L. Noschinski
 
−
# [http://bit.ly/1iJ8uVz A graph library for Isabelle]. ~ L. Noschinski
 
−
# [http://bit.ly/I0CU80 Gödel’s incompleteness theorems]. ~ L.C. Paulson
 
−
# [http://bit.ly/I0CPRN The hereditarily finite sets]. ~ L.C. Paulson
 
−
# [http://bit.ly/HBiIJI Applications of real number theorem proving in PVS]. ~ H. Gottliebsen, R. Hardy, O. Lightfoot y U. Martin
 
−
# [http://bit.ly/1awnMLB A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets]. ~ L.C. Paulson
 
−
# [http://bit.ly/19lWeYy Verified AIG algorithms in ACL2]. ~ J. Davis y S. Swords
 
−
# [http://bit.ly/GAhC00 A formal model and correctness proof for an access control policy framework]. ~ C. Wu, X. Zhang y C. Urban
 
−
# [http://bit.ly/16SMvSS The ontological argument in PVS]. ~ J. Rushby
 
−
# [http://bit.ly/1dRt9n0  Formalizing Moessner’s theorem and generalizations in Nuprl]. ~ M. Bickford, D. Kozen y A. Silva
 
−
# [http://bit.ly/1bSeDNB Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model]. ~ M. Ayala y Y. Santos
 
−
# [http://bit.ly/1feFqWE Proof assistant based on didactic considerations]. ~ J. Pais y A Tasistro
 
−
# [http://bit.ly/18tHNBi Theory exploration for interactive theorem proving]. ~ M. Johansson
 
−
# [http://bit.ly/1b0242s From Tarski to Hilbert]. ~ G. Braun y J. Narboux
 
−
# [http://bit.ly/18HaXaR Formal verification of language-based concurrent noninterference]. ~ A. Popescu, J. Hölzl y T. Nipkow
 
−
# [http://bit.ly/1aRTQsU A Traffic Alert and Collision Avoidance System(TCAS-II) Resolution Advisory Algorithm]. ~ C. Muñoz, A. Narkawicz y J. Chamberlain
 
−
# [http://bit.ly/1dNwhDI Formal verification of cryptographic security proofs]. ~ M. Berg
 
−
# [http://bit.ly/17muAUv Polygonal numbers in Mizar]. ~ A. Grabowski
 
−
# [http://bit.ly/1hk5z6L A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle]. ~ L.C. Paulson
 
−
# [http://bit.ly/1cSL0wE Steps towards verified implementations of HOL Light]. ~ M.O. Myreen, S. Owens y R. Kumar
 
−
# [http://bit.ly/16Kbgm0 Generic datatypes à la carte]. ~ S. Keuchel y T. Schrijvers
 
−
# [http://bit.ly/1bqJGx4 Proof pearl: A verified bignum implementation in x86-64 machine code]. ~ M.O. Myreen y G. Curello
 
−
# [http://bit.ly/142ow2Q Mechanized metatheory for a λ λ-calculus with trust types]. ~ R. Ribeiro, C. Camarão y L. Figueiredo
 
−
# [http://bit.ly/15WZBDy Proving soundness of combinatorial Vickrey auctions and generating verified executable code]. ~ M.B. Caminati, M. Kerber, C. Lange y C. Rowat
 
−
# [http://bit.ly/198g4n9 A computer-assisted proof of correctness of a marching cubes algorithm]. ~ A.N. Chernikov y J. Xu
 
−
# [http://bit.ly/11QA5g7 Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm]. ~ L. Lambán, J. Rubio, F.J. Martín y J.L. Ruiz
 
−
# [http://bit.ly/1cJAXYk The Königsberg bridge problem and the friendship theorem]. ~ W. Li
 
−
# [http://bit.ly/13DBK9R Formal verification of a proof procedure for the description logic ALC]. ~ M. Chaabani, M. Mezghiche y M. Strecker
 
−
# [http://bit.ly/1ep2ex9 Pratt’s primality certificates]. ~ S. Wimmer y L. Noschinski
 
−
# [http://bit.ly/13C95Ci Reasoning about higher-order relational specifications]. ~ Y. Wang, K. Chaudhuri, A. Gacek y G. Nadathur
 
−
# [http://bit.ly/18QQLcL Proofs you can believe in – Proving equivalences between Prolog semantics in Coq]. ~ J. Kriener, A. King y S. Blazy
 
−
# [http://bit.ly/19uc82J Certified, efficient and sharp univariate Taylor models in Coq]. ~ E. Martin-Dorel, L. Rideau, L. Théry, M. Mayero y I. Paşca
 
−
# [http://bit.ly/1c4Rzel Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁]. ~ M. Norrish y B. Huffman 
 
−
# [http://bit.ly/14b4Akz Program verification based on Kleene algebra in Isabelle/HOL] ~ A. Armstrong, G. Struth y T. Weber
 
−
# [http://bit.ly/1aOgRKx Reading an algebra textbook (by translating it to a formal document in the Isabelle/Isar language)]. ~ C. Ballarin
 
−
# [http://bit.ly/11HKixj Computational verification of network programs in Coq]. ~ G. Stewart
 
−
# [http://www.glc.us.es/~jalonso/vestigium/resena-certifying-homological-algorithms-to-study-biomedical-images Certifying homological algorithms to study biomedical images]. ~ M. Poza
 
−
# [http://bit.ly/16Nks9m Formalizing cut elimination of coalgebraic logics in Coq]. ~ H. Tews
 
−
# [http://www.glc.us.es/~jalonso/vestigium/resena-the-formalization-of-syntax-based-mathematical-algorithms-using-quotation-and-evaluation/ The formalization of syntax-based mathematical algorithms using quotation and evaluation]. ~ W.M. Farmer
 
−
# [http://www.glc.us.es/~jalonso/vestigium/resena-certified-symbolic-manipulation-bivariate-simplicial-polynomials/ Certified symbolic manipulation: Bivariate simplicial polynomials]. ~ L. Lambán, F.J. Martín, J. Rubio y J.L. Ruiz
 
−
# [http://www.glc.us.es/~jalonso/vestigium/resena-solveurs-cpfd-verifies-formellement/ Solveurs CP(FD) vérifiés formellement]. ~ C Dubois y A. Gotlieb
 
−
# [http://www.glc.us.es/~jalonso/vestigium/resena-formalizing-bounded-increase/ Formalizing bounded increase]. ~ R. Thiemann
 
−
# [http://www.glc.us.es/~jalonso/vestigium/resena-formal-mathematics-on-display-a-wiki-for-flyspeck/ Formal mathematics on display: A wiki for Flyspeck]. ~ C. Tankink, C. Kaliszyk, J. Urban y H. Geuvers
 
−
# [http://www.glc.us.es/~jalonso/vestigium/resena-theorem-of-three-circles-in-coq Theorem of three circles in Coq]. ~ J. Zsidó
 
−
# [http://bit.ly/19fiWAY Certified HLints with Isabelle/HOLCF-Prelude]. ~ J. Breitner, B. Huffman, N. Mitchell y C. Sternagel
 
−
# [http://bit.ly/ZfSQrQ Automatic data refinement]. ~ P. Lammich
 
−
# [http://bit.ly/18vyjm7 The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups)]. ~ A. Mahboubi
 
−
# [http://bit.ly/114oyZV Mechanical verification of SAT refutations with extended resolution]. ~ N. Wetzler, M.J.H. Heule y W.A. Hunt Jr.
 
−
# [http://bit.ly/13H0REu Type classes and filters for mathematical analysis in Isabelle/HOL] ~ J. Hölzl, F. Immler y B. Huffman
 
−
# [http://bit.ly/10fv8wO Verifying refutations with extended resolution]. ~ M. J. H. Heule, W. A. Hunt, Jr. y N. Wetzler 
 
−
# [http://bit.ly/10EcFWj A Web interface for Isabelle: The next generation]. ~ C. Lüth y M. Ring 
 
−
# [http://bit.ly/18P9CSv On the formalization of continuous-time Markov chains in HOL]. ~ L. Liu, O. Hasan y S. Tahar
 
−
# [http://bit.ly/17H2mqy Formalizing Turing machines]. ~ A. Asperti y W. Ricciotti
 
−
# [http://bit.ly/YwuCeL Light-weight containers for Isabelle: efficient, extensible, nestable]. ~ A. Lochbihler
 
−
# [http://bit.ly/10XLrRA Graph theory]. ~ L. Noschinski
 
−
# [http://bit.ly/19kPEP4 A machine-checked proof of the odd order theorem]. ~ G. Gonthier et als.
 
−
# [http://goo.gl/LdihL A constructive theory of regular languages in Coq]. ~ C. Doczkal, J.O. Kaiser y G. Smolka
 
−
# [http://goo.gl/gwcwL A formal proof of Kruskal’s tree theorem in Isabelle/HOL]. ~ C. Sternagel
 
−
# [http://goo.gl/CUF3e Formalizing Knuth-Bendix orders and Knuth-Bendix completion]. ~ C. Sternagel y R. Thiemann 
 
−
# [http://goo.gl/9JAfX Developing an auction theory toolbox]. ~ C. Lange, C. Rowat, W. Windsteiger y M. Kerber
 
−
# [http://goo.gl/6OfmQ Formalization of incremental simplex algorithm by stepwise refinement]. ~ M. Spasić y F. Marić 
 
−
# [http://goo.gl/Guxky Coinductive pearl: Modular first-order logic completeness]. ~ J.C. Blanchette, A. Popescu y D. Traytel
 
−
# [http://goo.gl/HUOl8 A fully verified executable LTL model checker]. ~ J. Esparza et als.
 
−
# [http://goo.gl/RV54S ForMaRE - formal mathematical reasoning in economics]. ~ M. Kerber, C. Lange y C. Rowat.
 
−
# [http://goo.gl/Y7sIq AI over large formal knowledge bases: The first decade]. ~ J. Urban.
 
−
# [http://goo.gl/vvqNg Formalization of real analysis: A survey of proof assistants and libraries]. ~ S. Boldo, C. Lelay y G. Melquiond.
 
−
# [http://goo.gl/bEFYa Data refinement in Isabelle/HOL]. ~ F. Haftmann, A. Krauss, O. Kunčar y T. Nipkow
 
−
# [http://goo.gl/xTyvE Formalizing the confluence of orthogonal rewriting systems]. ~ A.C. Rocha y M. Ayala.
 
−
# [http://goo.gl/zCYHj Formalization of the complex number theory in HOL4]. ~ Z. Shi et als.
 
−
# [http://goo.gl/kM0dI Programming and reasonning with PowerLists in Coq]. ~ F. Loulergue y V. Niculescu 
 
−
# [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
 

Revisión actual del 19:23 8 feb 2022

En esta página se recogen en enlaces que sirven de documentación al curso de demostración asistida por ordenador (DAO). Los enlaces están actualizados en el curso 2019-20.

Visiones generales de la DAO

  1. J.A. Alonso. Razonamiento formalizado: Del sueño a la realidad de las pruebas. Vestigium, 26 de diciembre de 2012.
  2. J. Avigad. Interactive theorem proving, automated reasoning, and mathematical computation. ICERM, 14 de diciembre de 2012.
  3. M. Davis. The early history of automated deduction.
  4. J.P. Delahaye Du rêve à la réalité des preuves. Interstices, 8 de julio de 2012.
  5. J. Germoni Coq et caractères: Preuve formelle du théorème de Feit et Thompson. Images des Mathématiques, CNRS, 23 de noviembre de 2012.
  6. H. Geuvers Proof assistants: History, ideas and future. Sadhana, Vol. 34-1, pp. 3-25, février 2009.
  7. G. Gonthier The four-color theorem. Notices of the AMS, Vol. 55, n° 11, pp. 1382-1393, 2008.
  8. T. Hales. Formal proof. Notices of AMS, Vol. 55, N. 11 (2008) pp. 1370-1380.
  9. J. Harrison. A short survey of automated reasoning. Lecture Notes in Computer Science, Vol. 4545, pp. 334-349, 2007.
  10. J. Harrison. Formal proof: Theory and practice. Notices of the AMS, Vol. 55, N. 11 (2008) p.1395-1406.
  11. G. Kolata. Computer math proof shows reasoning power. The New York Times, 10 de diciembre de 1996.
  12. D. MacKenzie Computers and the sociology of mathematical proof.
  13. G. Sutcliffe. What is automated theorem proving?.
  14. F. Wiedijk Formalizing the «top 100» of mathematical theorems.
  15. F. Wiedijk Formal proof - Getting started. Notices of the AMS, Vol. 55, n° 11, pp. 1408-1414, 2008.
  16. F. Wiedijk, The QED manifesto revisited. Studies in Logic, Grammar and Rhetoric, Vol. 10(23), pp. 121-133, 2007.

Referencias sobre Isabelle/HOL

  1. B. Grechuk Isabelle primer for mathematicians.
  2. T. Nipkow Programming and proving in Isabelle/HOL.
  3. T. Nipkow, M. Wenzel y L.C. Paulson A proof assistant for higher-order logic.
  4. Isabelle/HOL — Higher-Order Logic.
  5. Tutorials and manuals for Isabelle.

Lecturas complementarias

Programación funcional

  1. J.A. Alonso Temas de "Programación funcional". Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
  2. J.A. Alonso y M.J. Hidalgo Piensa en Haskell (Ejercicios de programación funcional con Haskell). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
  3. G. Hutton Programming in Haskell. Cambridge University Press, 2007.
  4. M. Lipovača ¡Aprende Haskell por el bien de todos!.

Lógica computacional

  1. J.A. Alonso Temas de "Lógica informática" (2012-13). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
  2. R. Bornat Proof and disproof in formal logic: an introduction for programmers. Oxford University Press, 2005.
  3. K. Broda, S. Eisenbach, H. Khoshnevisan y S. Vickers Reasoned programming. Imperial College, 1994.
  4. K. Doets y J. van Eijck The Haskell Road to Logic, Maths and Programming.
  5. M. Huth y M. Ryan Logic in computer science: Modelling and reasoning about systems. Cambridge University Press, 2004. (Incluye el tutor en la Red).

Cursos relacionados

Cursos con Isabelle/HOL

  1. Clemens Ballarin. Automatic Deduction. (Univ de Innsbruck, 2008).
  2. Clemens Ballarin y Gerwin Klein Introduction to the Isabelle Proof Assistant. (en el IJCAR-2004).
  3. Clemens Ballarin y Tjark Weber. Automated Theorem Proving in Isabelle/HOL. (Univ. de Innsbruck, 2006-07).
  4. A.D. Brucker, D. Basin, J.G. Smaus y B. Wolff. Computer-supported Modeling and Reasoning. (ETH Zurich, 2011).
  5. Mads Dam. Advanced formal methods. (KTH Royal Institute of Technology, 2007).
  6. Jacques Fleuriot y Paul Jackson. Automated reasoning. (Univ. de Edimburgo, 2012-13).
  7. Thomas Genet Software formal analysis and design. (Univ. de Rennes)
  8. Gerwin Klein. Theorem Proving - Principles, Techniques, Applications. (NICTA, 2004).
  9. Gerwin Klein. Advanced Topics in Software Verification. (NICTA, 2012).
  10. Joao Marcos. Lógica computacional: Demonstração assistida e semi-automática de teoremas.(UFRN, 2000).
  11. Tobias Nipkow. Semantics of programming languages. (Univ. de Munich, 2012-13).
  12. Tobias Nipkow Theorem Proving with Isabelle/HOL An Intensive Course.
  13. Larry Paulson. Interactive Formal Verification. (Univ. de Cambridge, 2009-10).
  14. Jan-Georg Smaus. Computer-supported modeling and reasoning. (Univ. de Feiburgo, 2009).
  15. Christian Sternagel Experiments in Verification – Introduction to Isabelle/HOL. (Univ. de Innsbruck, 2011-12).
  16. Tjark Weber. Interactive Formal Verification. (Univ. de Cambridge, 2010-11).

Otros cursos

  1. José A. Alonso Lógica informática (Univ. de Sevilla, 2012-13).
  2. Yves Bertot, Pierre Casteran, Benjamin Gregoire, Pierre Letouzey y Assia Mahboubi Modelling and verifying algorithms in Coq: an introduction. (INRIA Paris-Rocquencourt, 14-18 noviembre 2011).
  3. Pierre Castéran Logic (Master In Verification) (Univ. de Burdeos, 2011-12).
  4. Ian Hodkinson Logic (Imperial College, Londres, 2010-11).
  5. Peter Lucas Knowledge Representation and Reasoning (Radboud University # egen, 2011-12).
  6. Larry Paulson Logic and Proof (Univ. de Cambridge, 2011-12).
  7. Riccardo Pucella Logic and Computation (Northeastern University, 2009). Curso con ACL2.

Bibliotecas de ejemplos de verificación

  1. Archive of Formal Proofs.
  2. Formalizing 100 Theorems.
  3. Gallery of verified programs.
Obtenido de «https://www.glc.us.es/~jalonso/RA2017/index.php?title=Documentación&oldid=351»