Documentación"
De Razonamiento automático (2018-19)
Revisión del 14:32 20 oct 2018 de Jalonso (discusión | contribuciones) (Página creada con «En esta página se recogen en enlaces que sirven de documentación al curso de "Razonamiento automático" == Visiones generales de la DAO == # J.A. Alonso. [http://goo.gl…»)
En esta página se recogen en enlaces que sirven de documentación al curso de "Razonamiento automático"
Sumario
1 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.
- J. Gross Machine-checked proof. AMS Notices, 15 de octubre de 2017.
- 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.
- G. Sutcliffe. What is automated theorem proving?.
- 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.
2 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.
3 Lecturas complementarias
3.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!.
3.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).
4 Cursos relacionados
4.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).
4.2 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).
- 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).
- Pierre Castéran Logic (Master In Verification) (Univ. de Burdeos, 2011-12).
- Adam Chlipala Interactive computer theorem proving. (MIT, 2012-13).
- Adam Chlipala y Armando Solar Lezama Foundations of program analysis. (MIT, 2013-14).
- 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).
5 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.
6 Artículos recientes
Están en orden cronológico inverso a la fecha de su reseña en Vestigium:
- Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem. L. Noschinski
- A graph library for Isabelle. ~ L. Noschinski
- Gödel’s incompleteness theorems. ~ L.C. Paulson
- The hereditarily finite sets. ~ L.C. Paulson
- Applications of real number theorem proving in PVS. ~ H. Gottliebsen, R. Hardy, O. Lightfoot y U. Martin
- A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets. ~ L.C. Paulson
- Verified AIG algorithms in ACL2. ~ J. Davis y S. Swords
- A formal model and correctness proof for an access control policy framework. ~ C. Wu, X. Zhang y C. Urban
- The ontological argument in PVS. ~ J. Rushby
- Formalizing Moessner’s theorem and generalizations in Nuprl. ~ M. Bickford, D. Kozen y A. Silva
- Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model. ~ M. Ayala y Y. Santos
- Proof assistant based on didactic considerations. ~ J. Pais y A Tasistro
- Theory exploration for interactive theorem proving. ~ M. Johansson
- From Tarski to Hilbert. ~ G. Braun y J. Narboux
- Formal verification of language-based concurrent noninterference. ~ A. Popescu, J. Hölzl y T. Nipkow
- A Traffic Alert and Collision Avoidance System(TCAS-II) Resolution Advisory Algorithm. ~ C. Muñoz, A. Narkawicz y J. Chamberlain
- Formal verification of cryptographic security proofs. ~ M. Berg
- Polygonal numbers in Mizar. ~ A. Grabowski
- A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle. ~ L.C. Paulson
- Steps towards verified implementations of HOL Light. ~ M.O. Myreen, S. Owens y R. Kumar
- Generic datatypes à la carte. ~ S. Keuchel y T. Schrijvers
- Proof pearl: A verified bignum implementation in x86-64 machine code. ~ M.O. Myreen y G. Curello
- Mechanized metatheory for a λ λ-calculus with trust types. ~ R. Ribeiro, C. Camarão y L. Figueiredo
- Proving soundness of combinatorial Vickrey auctions and generating verified executable code. ~ M.B. Caminati, M. Kerber, C. Lange y C. Rowat
- A computer-assisted proof of correctness of a marching cubes algorithm. ~ A.N. Chernikov y J. Xu
- 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
- The Königsberg bridge problem and the friendship theorem. ~ W. Li
- Formal verification of a proof procedure for the description logic ALC. ~ M. Chaabani, M. Mezghiche y M. Strecker
- Pratt’s primality certificates. ~ S. Wimmer y L. Noschinski
- Reasoning about higher-order relational specifications. ~ Y. Wang, K. Chaudhuri, A. Gacek y G. Nadathur
- Proofs you can believe in – Proving equivalences between Prolog semantics in Coq. ~ J. Kriener, A. King y S. Blazy
- Certified, efficient and sharp univariate Taylor models in Coq. ~ E. Martin-Dorel, L. Rideau, L. Théry, M. Mayero y I. Paşca
- Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁. ~ M. Norrish y B. Huffman
- Program verification based on Kleene algebra in Isabelle/HOL ~ A. Armstrong, G. Struth y T. Weber
- Reading an algebra textbook (by translating it to a formal document in the Isabelle/Isar language). ~ C. Ballarin
- Computational verification of network programs in Coq. ~ G. Stewart
- Certifying homological algorithms to study biomedical images. ~ M. Poza
- Formalizing cut elimination of coalgebraic logics in Coq. ~ H. Tews
- The formalization of syntax-based mathematical algorithms using quotation and evaluation. ~ W.M. Farmer
- Certified symbolic manipulation: Bivariate simplicial polynomials. ~ L. Lambán, F.J. Martín, J. Rubio y J.L. Ruiz
- Solveurs CP(FD) vérifiés formellement. ~ C Dubois y A. Gotlieb
- Formalizing bounded increase. ~ R. Thiemann
- Formal mathematics on display: A wiki for Flyspeck. ~ C. Tankink, C. Kaliszyk, J. Urban y H. Geuvers
- Theorem of three circles in Coq. ~ J. Zsidó
- Certified HLints with Isabelle/HOLCF-Prelude. ~ J. Breitner, B. Huffman, N. Mitchell y C. Sternagel
- Automatic data refinement. ~ P. Lammich
- The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups). ~ A. Mahboubi
- Mechanical verification of SAT refutations with extended resolution. ~ N. Wetzler, M.J.H. Heule y W.A. Hunt Jr.
- Type classes and filters for mathematical analysis in Isabelle/HOL ~ J. Hölzl, F. Immler y B. Huffman
- Verifying refutations with extended resolution. ~ M. J. H. Heule, W. A. Hunt, Jr. y N. Wetzler
- A Web interface for Isabelle: The next generation. ~ C. Lüth y M. Ring
- On the formalization of continuous-time Markov chains in HOL. ~ L. Liu, O. Hasan y S. Tahar
- Formalizing Turing machines. ~ A. Asperti y W. Ricciotti
- Light-weight containers for Isabelle: efficient, extensible, nestable. ~ A. Lochbihler
- Graph theory. ~ L. Noschinski
- A machine-checked proof of the odd order theorem. ~ G. Gonthier et als.
- A constructive theory of regular languages in Coq. ~ C. Doczkal, J.O. Kaiser y G. Smolka
- A formal proof of Kruskal’s tree theorem in Isabelle/HOL. ~ C. Sternagel
- Formalizing Knuth-Bendix orders and Knuth-Bendix completion. ~ C. Sternagel y R. Thiemann
- Developing an auction theory toolbox. ~ C. Lange, C. Rowat, W. Windsteiger y M. Kerber
- Formalization of incremental simplex algorithm by stepwise refinement. ~ M. Spasić y F. Marić
- Coinductive pearl: Modular first-order logic completeness. ~ J.C. Blanchette, A. Popescu y D. Traytel
- A fully verified executable LTL model checker. ~ J. Esparza et als.
- ForMaRE - formal mathematical reasoning in economics. ~ M. Kerber, C. Lange y C. Rowat.
- AI over large formal knowledge bases: The first decade. ~ J. Urban.
- Formalization of real analysis: A survey of proof assistants and libraries. ~ S. Boldo, C. Lelay y G. Melquiond.
- Data refinement in Isabelle/HOL. ~ F. Haftmann, A. Krauss, O. Kunčar y T. Nipkow
- Formalizing the confluence of orthogonal rewriting systems. ~ A.C. Rocha y M. Ayala.
- Formalization of the complex number theory in HOL4. ~ Z. Shi et als.
- Programming and reasonning with PowerLists in Coq. ~ F. Loulergue y V. Niculescu
- A hierarchy of mathematical structures in ACL2. ~ J. Heras, F.J. Martín y V. Pascual.
- Mechanising Turing Machines and Computability Theory in Isabelle/HOL ~ J. Xu, X. Zhang y C. Urban