Acciones

Diferencia entre revisiones de «Documentación»

De Razonamiento automático (2019-20)
 
(No se muestran 28 ediciones intermedias del mismo usuario)
Línea 7: Línea 7:
== Visiones generales de la DAO ==
== Visiones generales de la DAO ==


# J.A. Alonso. [http://goo.gl/NWk7b Razonamiento formalizado: Del sueño a la realidad de las pruebas]. ''Vestigium'', 26 de diciembre de 2012.
# J.A. Alonso. [http://goo.gl/NWk7b Razonamiento formalizado: Del sueño a la realidad de las pruebas].  
# 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.M. Aransay y C. Domínguez. [http://gaceta.rsme.es/abrir.php?id=1057 Demostración asistida por ordenador].
# A. Asperti. [https://arxiv.org/abs/1701.03602 Automatic verification and interactive theorem proving].
# A. Asperti. [http://www.cs.unibo.it/~asperti/SLIDES/itp.pdf A survey on interactive theorem proving].
# J. Avigad. [http://bit.ly/1hsA8Ew Formal verification, interactive theorem proving, and automated reasoning].
# 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/london.pdf Automated reasoning for the working mathematician].
# J. Avigad, J. Harrison. [https://www.cl.cam.ac.uk/~jrh13/papers/cacm.pdf Formally verified Mathematics].
# H. Barendregt y F. Wiedijk. [http://ftp.science.ru.nl/CSI/CompMath.Found/Barendregt-Wiedijk.pdf The challenge of computer mathematics].
# K. Buzzard. [http://wwwf.imperial.ac.uk/~buzzard/one_off_lectures/msr.pdf The future of mathematics?]
# C.S. Calude y C. Müller [https://www.cs.auckland.ac.nz/~cristian/crispapers/56250217.pdf Formal proof: reconciling correctness and understanding].
# R. David. [http://www.lama.univ-savoie.fr/~david/ftp/amphis.pdf Peut-on faire des Mathématiques avec un ordinateur?]
# R. David y C. Raffalli. [http://www.lama.univ-savoie.fr/~david/ftp/amphi07.pdf Peut-on avoir confiance en l’informatique?]
# M. Davis. [http://www.cs.nyu.edu/cs/faculty/davism/early.ps The early history of automated deduction].
# M. Davis. [http://www.cs.nyu.edu/cs/faculty/davism/early.ps The early history of automated deduction].
# 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/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.cs.ru.nl/~herman/ictopen.pdf Can the computer really help us to prove theorems?]
# 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.
# J. Gross [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.  
# J. Harrison, J. Urban y F. Wiedijk [http://www.cl.cam.ac.uk/~jrh13/papers/joerg.pdf History of interactive theorem proving].
# A. Koutsoukou-Argyraki. [https://www.researchgate.net/profile/Angeliki_Koutsoukou-Argyraki/publication/334549483_FORMALISING_MATHEMATICS_-IN_PRAXIS_A_MATHEMATICIAN%27S_VERY_FIRST_EXPERIENCES_WITH_ISABELLEHOL/links/5d30f782299bf1547cc25f63/FORMALISING-MATHEMATICS-IN-PRAXIS-A-MATHEMATICIANS-VERY-FIRST-EXPERIENCES-WITH-ISABELLE-HOL.pdf Formalising Mathematics-in praxis; A mathematician's very first experiences with Isabelle/HOL]].
# 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].
# A. Mahboubi [https://jncf2018.lip6.fr/files/lecture-notes/jncf2018-mahboubi.pdf Calcul formel et preuves formelles].
# G. Sutcliffe. [http://www.cs.miami.edu/~tptp/OverviewOfATP.html What is automated theorem proving?].
# A. Mahboubi. [http://bit.ly/2ch3xEa Machine-checked mathematics].
# A. Mahboubi. [http://bit.ly/1qLTVBm Un ordinateur pour vérifier les preuves mathématiques].
# 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].
# C. Nalon. [https://www.mat.ufrn.br/cade-27/wp-content/uploads/2019/09/2019CN-CADE.pdf Machine-oriented reasoning].
# J. Narboux. [https://hal.inria.fr/hal-00809448/document Les assistants de preuve, ou comment avoir confiance en ses démonstrations].
# L.C. Paulson. [https://www.cl.cam.ac.uk/~lp15/papers/Formath/Sophia2017.pdf Proof assistants: from symbolic logic to real mathematics?]
# L.C. Paulson, T. Nipkow y M. Wenzel. [https://arxiv.org/abs/1907.02836 From LCF to Isabelle/HOL].
# T. Ringer et als. [https://arxiv.org/abs/2003.06458 QED at large: A survey of engineering of formally verified software]. 
# P. Schnider. [http://bit.ly/1Gxxmx6 An introduction to proof assistants].
# J. Schöpf y S. Widauer [http://cl-informatik.uibk.ac.at/teaching/ws17/vs/reports/SWreport.pdf History of interactive theorem proving].
# F.R. Villatoro. [http://francis.naukas.com/2017/07/29/la-demostracion-matematica-mas-larga La demostración matemática más larga].  
# 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 27: Línea 50:
== Referencias sobre Isabelle/HOL ==
== Referencias sobre Isabelle/HOL ==
# B. Blumson [https://philpapers.org/go.pl?id=BLUIFP&u=https%3A%2F%2Fphilpapers.org%2Farchive%2FBLUIFP.pdf Isabelle for philosophers].  
# B. Blumson [https://philpapers.org/go.pl?id=BLUIFP&u=https%3A%2F%2Fphilpapers.org%2Farchive%2FBLUIFP.pdf Isabelle for philosophers].  
# 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 [http://isabelle.in.tum.de/doc/tutorial.pdf A proof assistant for higher-order logic].
# A. Steen [https://git.imp.fu-berlin.de/leo-iii/compmeta_pub/raw/master/exercises/resources/Isabelle_ND_cheatsheet.pdf Mapping of ND proof templates to Isabelle formalization].
# [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://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].
# 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 [https://www.cs.us.es/~jalonso/cursos/i1m-19/temas/2019-20-I1M-temas-PF.pdf Temas de "Programación funcional"]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2019.
# 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://bit.ly/2pQofC2 Programming in Haskell]. Cambridge University Press, 2007.  
# M. Lipovača [http://aprendehaskell.es ¡Aprende Haskell por el bien de todos!].
# M. Lipovača [http://aprendehaskell.es ¡Aprende Haskell por el bien de todos!].
# M. Lipovaca y J. Brock [https://mybinder.org/v2/gh/jamesdbrock/learn-you-a-haskell-notebook/master?urlpath=lab/tree/learn_you_a_haskell/00-preface.ipynb Learn you a Haskell for great good!]
# T. Nipkow [https://www21.in.tum.de/teaching/fpv/WS1920/slides.pdf Functional programmingand verification]. TUM, 2019.


=== 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 [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.
# 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.
# K. Broda, S. Eisenbach, H. Khoshnevisan y S. Vickers [https://www.doc.ic.ac.uk/~susan/firstyearbook.pdf Reasoned programming]. Imperial College, 1994.
# 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://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]).
# 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]).


== 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).
Línea 70: Línea 89:
# 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].  
# 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 86: Línea 103:


=== 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).
# 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).  
# J. Blanchette y J. Höltz [https://lean-forward.github.io/logical-verification/2018 Logical verification]. (Vrije Universiteit Amsterdam, 2018-19).  
Línea 95: Línea 112:
# 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).


== Bibliotecas de ejemplos de verificación ==
== Bibliotecas de ejemplos de verificación ==
Línea 101: Línea 117:
# [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.tptp.org/ 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].


== Artículos recientes ==
== Artículos recientes ==
Línea 116: Línea 128:
== Ofertas de trabajo ==
== Ofertas de trabajo ==


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.
En [https://github.com/jaalonso/Trabajos-MULCIA/blob/master/README.org 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 19:08 8 feb 2022

En esta página se recogen en enlaces que sirven de documentación al curso de "Razonamiento automático"

Vídeos

Visiones generales de la DAO

  1. J.A. Alonso. Razonamiento formalizado: Del sueño a la realidad de las pruebas.
  2. J.M. Aransay y C. Domínguez. Demostración asistida por ordenador.
  3. A. Asperti. Automatic verification and interactive theorem proving.
  4. A. Asperti. A survey on interactive theorem proving.
  5. J. Avigad. Formal verification, interactive theorem proving, and automated reasoning.
  6. J. Avigad. Interactive theorem proving, automated reasoning, and mathematical computation. ICERM, 14 de diciembre de 2012.
  7. J. Avigad. Automated reasoning for the working mathematician.
  8. J. Avigad, J. Harrison. Formally verified Mathematics.
  9. H. Barendregt y F. Wiedijk. The challenge of computer mathematics.
  10. K. Buzzard. The future of mathematics?
  11. C.S. Calude y C. Müller Formal proof: reconciling correctness and understanding.
  12. R. David. Peut-on faire des Mathématiques avec un ordinateur?
  13. R. David y C. Raffalli. Peut-on avoir confiance en l’informatique?
  14. M. Davis. The early history of automated deduction.
  15. J.P. Delahaye Du rêve à la réalité des preuves. Interstices, 8 de julio de 2012.
  16. 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.
  17. H. Geuvers Proof assistants: History, ideas and future. Sadhana, Vol. 34-1, pp. 3-25, février 2009.
  18. H. Geuvers. Can the computer really help us to prove theorems?
  19. G. Gonthier The four-color theorem. Notices of the AMS, Vol. 55, n° 11, pp. 1382-1393, 2008.
  20. T. Hales. Formal proof. Notices of AMS, Vol. 55, N. 11 (2008) pp. 1370-1380.
  21. J. Harrison. A short survey of automated reasoning. Lecture Notes in Computer Science, Vol. 4545, pp. 334-349, 2007.
  22. J. Harrison. Formal proof: Theory and practice. Notices of the AMS, Vol. 55, N. 11 (2008) p.1395-1406.
  23. J. Harrison, J. Urban y F. Wiedijk History of interactive theorem proving.
  24. A. Koutsoukou-Argyraki. Formalising Mathematics-in praxis; A mathematician's very first experiences with Isabelle/HOL].
  25. G. Kolata. Computer math proof shows reasoning power. The New York Times, 10 de diciembre de 1996.
  26. A. Mahboubi Calcul formel et preuves formelles.
  27. A. Mahboubi. Machine-checked mathematics.
  28. A. Mahboubi. Un ordinateur pour vérifier les preuves mathématiques.
  29. D. MacKenzie Computers and the sociology of mathematical proof.
  30. C. Nalon. Machine-oriented reasoning.
  31. J. Narboux. Les assistants de preuve, ou comment avoir confiance en ses démonstrations.
  32. L.C. Paulson. Proof assistants: from symbolic logic to real mathematics?
  33. L.C. Paulson, T. Nipkow y M. Wenzel. From LCF to Isabelle/HOL.
  34. T. Ringer et als. QED at large: A survey of engineering of formally verified software.
  35. P. Schnider. An introduction to proof assistants.
  36. J. Schöpf y S. Widauer History of interactive theorem proving.
  37. F.R. Villatoro. La demostración matemática más larga.
  38. F. Wiedijk Formalizing the «top 100» of mathematical theorems.
  39. F. Wiedijk Formal proof - Getting started. Notices of the AMS, Vol. 55, n° 11, pp. 1408-1414, 2008.
  40. 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. Blumson Isabelle for philosophers.
  2. B. Grechuk Isabelle primer for mathematicians.
  3. T. Nipkow Programming and proving in Isabelle/HOL.
  4. T. Nipkow, M. Wenzel y L.C. Paulson A proof assistant for higher-order logic.
  5. A. Steen Mapping of ND proof templates to Isabelle formalization.
  6. Isabelle/HOL — Higher-Order Logic.
  7. M. Wenzel The Isabelle/Isar Reference Manual.
  8. M. Wenzel The Isabelle/Isar quick reference.
  9. 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, 2019.
  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!.
  5. M. Lipovaca y J. Brock Learn you a Haskell for great good!
  6. T. Nipkow Functional programmingand verification. TUM, 2019.

Lógica computacional

  1. J.A. Alonso Temas de "Lógica informática" (2015-16). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2015.
  2. K. Broda, S. Eisenbach, H. Khoshnevisan y S. Vickers Reasoned programming. Imperial College, 1994.
  3. 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. Automated reasoning. (Univ. de Edimburgo, 2016-17).
  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. Arnd Poetzsch-Heffter. Specification and Verification with Higher-Order Logic.
  15. Jan-Georg Smaus. Computer-supported modeling and reasoning. (Univ. de Feiburgo, 2009).
  16. Christian Sternagel Experiments in Verification – Introduction to Isabelle/HOL. (Univ. de Innsbruck, 2011-12).
  17. Tjark Weber. Interactive Formal Verification. (Univ. de Cambridge, 2010-11).

Cursos con Coq

  1. 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).
  2. Adam Chlipala Interactive computer theorem proving. (MIT, 2012-13).
  3. Adam Chlipala y Armando Solar Lezama Foundations of program analysis. (MIT, 2013-14).
  4. M. Greenberg Discrete mathematics and functional programming.
  5. Benjamin C. Pierce et als. Software foundations (Vol. 1: Logical foundations).
  6. Benjamin C. Pierce Software foundations (Univ. de Pensilvania, 2018).
  7. G. Smolka Introduction to computational logic (Univ. de Sarre, 2018).

Otros cursos

  1. José A. Alonso Lógica informática (Univ. de Sevilla, 2012-13).
  2. Thorsten Altenkirch y Peter Morris Introduction to formal reasoning (Univ. de Nottingham, 2010-11).
  3. J. Blanchette y J. Höltz Logical verification. (Vrije Universiteit Amsterdam, 2018-19).
  4. Pierre Castéran Logic (Master In Verification) (Univ. de Burdeos, 2011-12).
  5. Robby Findler Certified programming with dependent types. (Northwestern, 2013-14).
  6. Carlos Luna y Gustavo Betarte. Construcción formal de programas en teoría de tipos. (Univ. de la República, Uruguay, 2013-14).
  7. Ian Hodkinson Logic (Imperial College, Londres, 2010-11).
  8. Peter Lucas Knowledge Representation and Reasoning (Radboud University # egen, 2011-12).
  9. Larry Paulson Logic and Proof (Univ. de Cambridge, 2011-12).

Bibliotecas de ejemplos de verificación

  1. Archive of Formal Proofs.
  2. Formalizing 100 Theorems.
  3. Gallery of verified programs.
  4. The TPTP Problem Library for Automated Theorem Proving.

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.

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.

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