Razonamiento Automático (2022-23)
Temas
Ejercicios
Sistemas
Documentación
Trabajos
Entrar

Visiones generales del Razonamiento Automático

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

Bibliotecas de ejemplos de verificación

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