Documentación

En esta página se recogen en enlaces que sirven de documentación al curso de Demostración automática de teoremas (DAT).

Visiones generales

1. J. Aransay y C. Domínguez. Demostración asistida por ordenador.
2. J. Avigad. Interactive theorem proving, automated reasoning, and mathematical computation. ICERM, 14 de diciembre de 2012.
3. J. Harrison. A short survey of automated reasoning. Lecture Notes in Computer Science, Vol. 4545, pp. 334-349, 2007.
4. J. Harrison. Formal proof: Theory and practice. Notices of the AMS, Vol. 55, N. 11 (2008) p.1395-1406.

Referencias sobre Isabelle/HOL

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

Cursos relacionados

Cursos con Isabelle/HOL

1. Tobias Nipkow. Semantics of programming languages. (Univ. de Munich, 2012-13).
2. Tobias Nipkow Theorem Proving with Isabelle/HOL An Intensive Course.
3. Larry Paulson. Interactive Formal Verification. (Univ. de Cambridge, 2009-10).
4. Jeremy G. Siek. Theorem proving in Isabelle.(Univ. de Colorado, 2011).
5. Tjark Weber. Interactive Formal Verification. (Univ. de Cambridge, 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

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