Acciones

Documentación

De Razonamiento automático (2013-14)

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. 5 de diciembre de 2013.
  3. T. Nipkow, M. Wenzel y L.C. Paulson A proof assistant for higher-order logic. Springer-Verlag. 5 de diciembre de 2013.
  4. Isabelle/HOL — Higher-Order Logic. 5 de diciembre de 2013.
  5. M. Wenzel The Isabelle/Isar Reference Manual. 5 de diciembre de 2013.
  6. M. Wenzel The Isabelle/Isar quick reference.
  7. J. Siek Quick Reference for Isabelle/Isar Propositional Logic.
  8. J. Siek Quick Reference for Isabelle/Isar More Proof Techniques.
  9. J. Siek Quick Reference for Isabelle/Isar First-Order Logic.
  10. Tutorials and manuals for Isabelle2013.

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. Jeremy Avigad. Logic and Formal Verification. (Carnegie Mellon, 2009).
  2. Clemens Ballarin. Automatic Deduction. (Univ de Innsbruck, 2008).
  3. Clemens Ballarin. Introduction to the Isabelle Proof Assistant. (Belgrado, 2008).
  4. Clemens Ballarin y Gerwin Klein Introduction to the Isabelle Proof Assistant. (en el IJCAR-2004).
  5. Clemens Ballarin y Tjark Weber. Automated Theorem Proving in Isabelle/HOL. (Univ. de Innsbruck, 2006-07).
  6. A.D. Brucker, D. Basin, J.G. Smaus y B. Wolff. Computer-supported Modeling and Reasoning. (ETH Zurich, 2011).
  7. Mads Dam. Advanced formal methods. (KTH Royal Institute of Technology, 2007).
  8. Jacques Fleuriot y Paul Jackson. Automated reasoning. (Univ. de Edimburgo, 2012-13).
  9. Thomas Genet Software formal analysis and design. (Univ. de Rennes)
  10. Gerwin Klein. Theorem Proving - Principles, Techniques, Applications. (NICTA, 2004).
  11. Gerwin Klein. Advanced Topics in Software Verification. (NICTA, 2012).
  12. Joao Marcos. Lógica computacional: Demonstração assistida e semi-automática de teoremas.(UFRN, 2000).
  13. Tobias Nipkow. Semantics of programming languages. (Univ. de Munich, 2012-13).
  14. Tobias Nipkow Theorem Proving with Isabelle/HOL An Intensive Course.
  15. Larry Paulson. Interactive Formal Verification. (Univ. de Cambridge, 2009-10).
  16. Arnd Poetzsch-Heffter. Specification and Verification with Higher-Order Logic.
  17. Viorel Preoteasa, Ralph-Johan Back y Charmi Panchal. Introduction to mechanized reasoning with Isabelle/HOL. (Åbo Akademi University, 2012).
  18. Jeremy G. Siek. Practical Theorem Proving with Isabelle/Isar. (Univ. de Colorado, 2007).
  19. Jeremy G. Siek. Theorem proving in Isabelle. (Univ. de Colorado, 2011).
  20. Jan-Georg Smaus. Computer-supported modeling and reasoning. (Univ. de Feiburgo, 2009).
  21. Christian Sternagel Experiments in Verification – Introduction to Isabelle/HOL. (Univ. de Innsbruck, 2011-12).
  22. 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. Adam Chlipala Interactive computer theorem proving. (MIT, 2012-13).
  5. Adam Chlipala y Armando Solar Lezama Foundations of program analysis. (MIT, 2013-14).
  6. Robby Findler Certified programming with dependent types. (Northwestern, 2013-14).
  7. Nuno Gaspar Verification with the Coq Proof Assistant (INRIA Sophia Antipolis, 2012-13).
  8. Carlos Luna y Gustavo Betarte. Construcción formal de programas en teoría de tipos. (Univ. de la República, Uruguay, 2013-14).
  9. Michael Genesereth Computational Logic (Univ. de Stanford, 2011-12).
  10. Ian Hodkinson Logic (Imperial College, Londres, 2010-11).
  11. Peter Lucas Knowledge Representation and Reasoning (Radboud University # egen, 2011-12).
  12. Larry Paulson Logic and Proof (Univ. de Cambridge, 2011-12).
  13. Michael Winter [Logic in Computer Science] (Brock University, Ontario, Canada, 2010-11).

Bibliotecas de ejemplos de verificación

  1. Archive of Formal Proofs.
  2. Formalizing 100 Theorems.
  3. Gallery of verified programs.
  4. Induction Challenge Problems.
  5. Larry Wos' Notebooks.
  6. The TPTP Problem Library for Automated Theorem Proving.
  7. The 1st Verified Software Competition.
  8. The 2nd Verified Software Competition.
  9. VerifyThis (A collection of verification benchmarks.

Artículos recientes

Están en orden cronológico inverso a la fecha de su reseña en Vestigium:

  1. Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem. L. Noschinski
  2. A graph library for Isabelle. ~ L. Noschinski
  3. Gödel’s incompleteness theorems. ~ L.C. Paulson
  4. The hereditarily finite sets. ~ L.C. Paulson
  5. Applications of real number theorem proving in PVS. ~ H. Gottliebsen, R. Hardy, O. Lightfoot y U. Martin
  6. A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets. ~ L.C. Paulson
  7. Verified AIG algorithms in ACL2. ~ J. Davis y S. Swords
  8. A formal model and correctness proof for an access control policy framework. ~ C. Wu, X. Zhang y C. Urban
  9. The ontological argument in PVS. ~ J. Rushby
  10. Formalizing Moessner’s theorem and generalizations in Nuprl. ~ M. Bickford, D. Kozen y A. Silva
  11. Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model. ~ M. Ayala y Y. Santos
  12. Proof assistant based on didactic considerations. ~ J. Pais y A Tasistro
  13. Theory exploration for interactive theorem proving. ~ M. Johansson
  14. From Tarski to Hilbert. ~ G. Braun y J. Narboux
  15. Formal verification of language-based concurrent noninterference. ~ A. Popescu, J. Hölzl y T. Nipkow
  16. A Traffic Alert and Collision Avoidance System(TCAS-II) Resolution Advisory Algorithm. ~ C. Muñoz, A. Narkawicz y J. Chamberlain
  17. Formal verification of cryptographic security proofs. ~ M. Berg
  18. Polygonal numbers in Mizar. ~ A. Grabowski
  19. A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle. ~ L.C. Paulson
  20. Steps towards verified implementations of HOL Light. ~ M.O. Myreen, S. Owens y R. Kumar
  21. Generic datatypes à la carte. ~ S. Keuchel y T. Schrijvers
  22. Proof pearl: A verified bignum implementation in x86-64 machine code. ~ M.O. Myreen y G. Curello
  23. Mechanized metatheory for a λ λ-calculus with trust types. ~ R. Ribeiro, C. Camarão y L. Figueiredo
  24. Proving soundness of combinatorial Vickrey auctions and generating verified executable code. ~ M.B. Caminati, M. Kerber, C. Lange y C. Rowat
  25. A computer-assisted proof of correctness of a marching cubes algorithm. ~ A.N. Chernikov y J. Xu
  26. 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
  27. The Königsberg bridge problem and the friendship theorem. ~ W. Li
  28. Formal verification of a proof procedure for the description logic ALC. ~ M. Chaabani, M. Mezghiche y M. Strecker
  29. Pratt’s primality certificates. ~ S. Wimmer y L. Noschinski
  30. Reasoning about higher-order relational specifications. ~ Y. Wang, K. Chaudhuri, A. Gacek y G. Nadathur
  31. Proofs you can believe in – Proving equivalences between Prolog semantics in Coq. ~ J. Kriener, A. King y S. Blazy
  32. Certified, efficient and sharp univariate Taylor models in Coq. ~ E. Martin-Dorel, L. Rideau, L. Théry, M. Mayero y I. Paşca
  33. Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁. ~ M. Norrish y B. Huffman
  34. Program verification based on Kleene algebra in Isabelle/HOL ~ A. Armstrong, G. Struth y T. Weber
  35. Reading an algebra textbook (by translating it to a formal document in the Isabelle/Isar language). ~ C. Ballarin
  36. Computational verification of network programs in Coq. ~ G. Stewart
  37. Certifying homological algorithms to study biomedical images. ~ M. Poza
  38. Formalizing cut elimination of coalgebraic logics in Coq. ~ H. Tews
  39. The formalization of syntax-based mathematical algorithms using quotation and evaluation. ~ W.M. Farmer
  40. Certified symbolic manipulation: Bivariate simplicial polynomials. ~ L. Lambán, F.J. Martín, J. Rubio y J.L. Ruiz
  41. Solveurs CP(FD) vérifiés formellement. ~ C Dubois y A. Gotlieb
  42. Formalizing bounded increase. ~ R. Thiemann
  43. Formal mathematics on display: A wiki for Flyspeck. ~ C. Tankink, C. Kaliszyk, J. Urban y H. Geuvers
  44. Theorem of three circles in Coq. ~ J. Zsidó
  45. Certified HLints with Isabelle/HOLCF-Prelude. ~ J. Breitner, B. Huffman, N. Mitchell y C. Sternagel
  46. Automatic data refinement. ~ P. Lammich
  47. The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups). ~ A. Mahboubi
  48. Mechanical verification of SAT refutations with extended resolution. ~ N. Wetzler, M.J.H. Heule y W.A. Hunt Jr.
  49. Type classes and filters for mathematical analysis in Isabelle/HOL ~ J. Hölzl, F. Immler y B. Huffman
  50. Verifying refutations with extended resolution. ~ M. J. H. Heule, W. A. Hunt, Jr. y N. Wetzler
  51. A Web interface for Isabelle: The next generation. ~ C. Lüth y M. Ring
  52. On the formalization of continuous-time Markov chains in HOL. ~ L. Liu, O. Hasan y S. Tahar
  53. Formalizing Turing machines. ~ A. Asperti y W. Ricciotti
  54. Light-weight containers for Isabelle: efficient, extensible, nestable. ~ A. Lochbihler
  55. Graph theory. ~ L. Noschinski
  56. A machine-checked proof of the odd order theorem. ~ G. Gonthier et als.
  57. A constructive theory of regular languages in Coq. ~ C. Doczkal, J.O. Kaiser y G. Smolka
  58. A formal proof of Kruskal’s tree theorem in Isabelle/HOL. ~ C. Sternagel
  59. Formalizing Knuth-Bendix orders and Knuth-Bendix completion. ~ C. Sternagel y R. Thiemann
  60. Developing an auction theory toolbox. ~ C. Lange, C. Rowat, W. Windsteiger y M. Kerber
  61. Formalization of incremental simplex algorithm by stepwise refinement. ~ M. Spasić y F. Marić
  62. Coinductive pearl: Modular first-order logic completeness. ~ J.C. Blanchette, A. Popescu y D. Traytel
  63. A fully verified executable LTL model checker. ~ J. Esparza et als.
  64. ForMaRE - formal mathematical reasoning in economics. ~ M. Kerber, C. Lange y C. Rowat.
  65. AI over large formal knowledge bases: The first decade. ~ J. Urban.
  66. Formalization of real analysis: A survey of proof assistants and libraries. ~ S. Boldo, C. Lelay y G. Melquiond.
  67. Data refinement in Isabelle/HOL. ~ F. Haftmann, A. Krauss, O. Kunčar y T. Nipkow
  68. Formalizing the confluence of orthogonal rewriting systems. ~ A.C. Rocha y M. Ayala.
  69. Formalization of the complex number theory in HOL4. ~ Z. Shi et als.
  70. Programming and reasonning with PowerLists in Coq. ~ F. Loulergue y V. Niculescu
  71. A hierarchy of mathematical structures in ACL2. ~ J. Heras, F.J. Martín y V. Pascual.
  72. Mechanising Turing Machines and Computability Theory in Isabelle/HOL ~ J. Xu, X. Zhang y C. Urban
Obtenido de «https://www.glc.us.es/~jalonso/RA2013/index.php?title=Documentación&oldid=701»