Diferencia entre revisiones de «Documentación»
De Razonamiento automático (2018-19)
(No se muestran 11 ediciones intermedias del mismo usuario) | |||
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 "Razonamiento automático". Los enlaces están actualizados en el [https://www.glc.us.es/~jalonso/RA2019/index.php/Documentaci%C3%B3n curso 2019-20]. |
+ | |||
+ | == Vídeos == | ||
+ | |||
+ | * Vídeos de deducción natural con Pandora: [http://bit.ly/1tqZIOe ejemplo 1] y [http://bit.ly/1nWAVp4 ejemplo 2]. | ||
== Visiones generales de la DAO == | == Visiones generales de la DAO == | ||
Línea 10: | Línea 14: | ||
# 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/article/fulltext/sadh/034/01/0003-0025 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. | ||
− | |||
# 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. | ||
Línea 16: | Línea 19: | ||
# 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 [http://www.bcs.org/server.php?show=ConWebDoc.4364 Computers and the sociology of mathematical proof]. | ||
− | |||
# 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. | ||
Línea 70: | Línea 72: | ||
# 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). | ||
# Tjark Weber. [http://www.cl.cam.ac.uk/teaching/1011/L21/ Interactive Formal Verification]. (Univ. de Cambridge, 2010-11). | # Tjark Weber. [http://www.cl.cam.ac.uk/teaching/1011/L21/ Interactive Formal Verification]. (Univ. de Cambridge, 2010-11). | ||
+ | |||
+ | === Cursos con Coq === | ||
+ | # 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). | ||
+ | # 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). | ||
+ | # M. Greenberg [http://www.cs.pomona.edu/~michael/courses/csci054s18/ Discrete mathematics and functional programming]. | ||
+ | # Benjamin C. Pierce et als. [https://softwarefoundations.cis.upenn.edu/lf-current/index.html Software foundations (Vol. 1: Logical foundations)]. | ||
+ | # Benjamin C. Pierce [https://www.seas.upenn.edu/~cis500/current/index.html Software foundations] (Univ. de Pensilvania, 2018). | ||
+ | # G. Smolka [https://courses.ps.uni-saarland.de/icl_18/2/Resources Introduction to computational logic] (Univ. de Sarre, 2018). | ||
=== 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/ 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). | # Thorsten Altenkirch y Peter Morris [http://www.cs.nott.ac.uk/~txa/g52ifr Introduction to formal reasoning] (Univ. de Nottingham, 2010-11). | ||
− | # | + | # J. Blanchette y J. Höltz [https://lean-forward.github.io/logical-verification/2018 Logical verification]. (Vrije Universiteit Amsterdam, 2018-19). |
# 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). | ||
− | |||
− | |||
# Robby Findler [http://www.eecs.northwestern.edu/~robby/courses/395-495-2013-fall Certified programming with dependent types]. (Northwestern, 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). | # 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). | ||
Línea 99: | Línea 108: | ||
Hay dos listas de artículos recientes: | Hay dos listas de artículos recientes: | ||
− | * en [https://twitter.com/search? | + | * en [https://twitter.com/search?f=tweets&q=%23ITP%20OR%20%23IsabelleHOL%20OR%20%23Coq%20OR%20%23Agda%20OR%20%23LeanProver%20OR%20%23MULCIA%20from%3AJose_A_Alonso&src=typd Twitter] que contiene enlaces a los artículos de razonamiento automático y demostración asistida por ordenador que se están publicando y |
* en [https://www.glc.us.es/~jalonso/vestigium/category/resena/ Vestigium] que contiene una reseña de los más destacados. | * en [https://www.glc.us.es/~jalonso/vestigium/category/resena/ Vestigium] que contiene una reseña de los más destacados. | ||
== Ofertas de trabajo == | == Ofertas de trabajo == | ||
− | En [https://github.com/jaalonso | + | En [https://github.com/jaalonso/Trabajos-MULCIA GitHub] se encuentra una recopilaciónn las ofertas de trabajo de interés para los estudiantes del Máster Universitario en Lógica, Computación e Inteligencia Artificial de la Universidad de Sevilla. |
Están en orden cronológico inverso por la fecha de su publicación en [https://twitter.com/search?l=&q=%23MULCIA%20from%3AJose_A_Alonso&src=typd&lang=es Twitter]. | Están en orden cronológico inverso por la fecha de su publicación en [https://twitter.com/search?l=&q=%23MULCIA%20from%3AJose_A_Alonso&src=typd&lang=es Twitter]. |
Revisión actual del 18:24 8 feb 2022
En esta página se recogen en enlaces que sirven de documentación al curso de "Razonamiento automático". Los enlaces están actualizados en el curso 2019-20.
Sumario
1 Vídeos
2 Visiones generales de la DAO
- J.A. Alonso. Razonamiento formalizado: Del sueño a la realidad de las pruebas. Vestigium, 26 de diciembre de 2012.
- J. Avigad. Interactive theorem proving, automated reasoning, and mathematical computation. ICERM, 14 de diciembre de 2012.
- M. Davis. The early history of automated deduction.
- J.P. Delahaye Du rêve à la réalité des preuves. Interstices, 8 de julio de 2012.
- 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.
- H. Geuvers Proof assistants: History, ideas and future. Sadhana, Vol. 34-1, pp. 3-25, février 2009.
- G. Gonthier The four-color theorem. Notices of the AMS, Vol. 55, n° 11, pp. 1382-1393, 2008.
- T. Hales. Formal proof. Notices of AMS, Vol. 55, N. 11 (2008) pp. 1370-1380.
- 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.
- G. Kolata. Computer math proof shows reasoning power. The New York Times, 10 de diciembre de 1996.
- D. MacKenzie Computers and the sociology of mathematical proof.
- F. Wiedijk Formalizing the «top 100» of mathematical theorems.
- F. Wiedijk Formal proof - Getting started. Notices of the AMS, Vol. 55, n° 11, pp. 1408-1414, 2008.
- F. Wiedijk, The QED manifesto revisited. Studies in Logic, Grammar and Rhetoric, Vol. 10(23), pp. 121-133, 2007.
3 Referencias sobre Isabelle/HOL
- B. Grechuk Isabelle primer for mathematicians.
- T. Nipkow Programming and proving in Isabelle/HOL.
- T. Nipkow, M. Wenzel y L.C. Paulson A proof assistant for higher-order logic.
- Isabelle/HOL — Higher-Order Logic.
- 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 Isabelle.
4 Lecturas complementarias
4.1 Programación funcional
- J.A. Alonso Temas de "Programación funcional". Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2016.
- 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.
- G. Hutton Programming in Haskell. Cambridge University Press, 2007.
- M. Lipovača ¡Aprende Haskell por el bien de todos!.
4.2 Lógica computacional
- J.A. Alonso Temas de "Lógica informática" (2015-16). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2015.
- K. Broda, S. Eisenbach, H. Khoshnevisan y S. Vickers Reasoned programming. Imperial College, 1994.
- K. Doets y J. van Eijck The Haskell Road to Logic, Maths and Programming.
- M. Huth y M. Ryan Logic in computer science: Modelling and reasoning about systems. Cambridge University Press, 2004. (Incluye el tutor en la Red).
5 Cursos relacionados
5.1 Cursos con Isabelle/HOL
- Jeremy Avigad. Logic and Formal Verification. (Carnegie Mellon, 2009).
- Clemens Ballarin. Automatic Deduction. (Univ de Innsbruck, 2008).
- Clemens Ballarin. Introduction to the Isabelle Proof Assistant. (Belgrado, 2008).
- Clemens Ballarin y Gerwin Klein Introduction to the Isabelle Proof Assistant. (en el IJCAR-2004).
- Clemens Ballarin y Tjark Weber. Automated Theorem Proving in Isabelle/HOL. (Univ. de Innsbruck, 2006-07).
- Jasmin Blanchette, Mathias Fleury y Daniel Wand Concrete semantics with Isabelle/HOL. (Univ. del Sarre, 2015-16).
- A.D. Brucker, D. Basin, J.G. Smaus y B. Wolff. Computer-supported Modeling and Reasoning. (ETH Zurich, 2011).
- Mads Dam. Advanced formal methods. (KTH Royal Institute of Technology, 2007).
- Jacques Fleuriot. Automated reasoning. (Univ. de Edimburgo, 2016-17).
- Thomas Genet Software formal analysis and design. (Univ. de Rennes)
- Gerwin Klein. Theorem Proving - Principles, Techniques, Applications. (NICTA, 2004).
- Gerwin Klein. Advanced Topics in Software Verification. (NICTA, 2012).
- Joao Marcos. Lógica computacional: Demonstração assistida e semi-automática de teoremas.(UFRN, 2000).
- 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).
- Arnd Poetzsch-Heffter. Specification and Verification with Higher-Order Logic.
- Jeremy G. Siek. Practical Theorem Proving with Isabelle/Isar. (Univ. de Colorado, 2007).
- Jeremy G. Siek. Theorem proving in Isabelle. (Univ. de Colorado, 2011).
- Jan-Georg Smaus. Computer-supported modeling and reasoning. (Univ. de Feiburgo, 2009).
- Christian Sternagel Experiments in Verification – Introduction to Isabelle/HOL. (Univ. de Innsbruck, 2011-12).
- Tjark Weber. Interactive Formal Verification. (Univ. de Cambridge, 2010-11).
5.2 Cursos con Coq
- 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).
- Adam Chlipala Interactive computer theorem proving. (MIT, 2012-13).
- Adam Chlipala y Armando Solar Lezama Foundations of program analysis. (MIT, 2013-14).
- M. Greenberg Discrete mathematics and functional programming.
- Benjamin C. Pierce et als. Software foundations (Vol. 1: Logical foundations).
- Benjamin C. Pierce Software foundations (Univ. de Pensilvania, 2018).
- G. Smolka Introduction to computational logic (Univ. de Sarre, 2018).
5.3 Otros cursos
- José A. Alonso Lógica informática (Univ. de Sevilla, 2012-13).
- Thorsten Altenkirch y Peter Morris Introduction to formal reasoning (Univ. de Nottingham, 2010-11).
- J. Blanchette y J. Höltz Logical verification. (Vrije Universiteit Amsterdam, 2018-19).
- Pierre Castéran Logic (Master In Verification) (Univ. de Burdeos, 2011-12).
- Robby Findler Certified programming with dependent types. (Northwestern, 2013-14).
- Carlos Luna y Gustavo Betarte. Construcción formal de programas en teoría de tipos. (Univ. de la República, Uruguay, 2013-14).
- Ian Hodkinson Logic (Imperial College, Londres, 2010-11).
- Peter Lucas Knowledge Representation and Reasoning (Radboud University # egen, 2011-12).
- Larry Paulson Logic and Proof (Univ. de Cambridge, 2011-12).
- David Pichardie Méthode de vérification (Universidad de Rennes, 2006-07).
6 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.
- The 1st Verified Software Competition.
- The 2nd Verified Software Competition.
- VerifyThis (A collection of verification benchmarks.
7 Artículos recientes
Hay dos listas de artículos recientes:
- en Twitter que contiene enlaces a los artículos de razonamiento automático y demostración asistida por ordenador que se están publicando y
- en Vestigium que contiene una reseña de los más destacados.
8 Ofertas de trabajo
En GitHub se encuentra una recopilaciónn las ofertas de trabajo de interés para los estudiantes del Máster Universitario en Lógica, Computación e Inteligencia Artificial de la Universidad de Sevilla.
Están en orden cronológico inverso por la fecha de su publicación en Twitter.