Documentación - Historial de revisiones

Jalonso en 17:22 8 feb 2022

2022-02-08T17:22:32Z

Jalonso en 12:50 8 feb 2022

2022-02-08T12:50:32Z

Mostrar los cambios

Jalonso: /* Referencias sobre Isabelle/HOL */

2015-12-23T15:16:56Z

‎Referencias sobre Isabelle/HOL

Jalonso: /* Referencias sobre Isabelle/HOL */

2015-12-23T15:15:40Z

‎Referencias sobre Isabelle/HOL

Jalonso: /* Referencias sobre Isabelle/HOL */

2015-12-23T15:12:14Z

‎Referencias sobre Isabelle/HOL

WikiSysop: Página creada con 'En esta página se recogen en enlaces que sirven de documentación al curso de demostración asistida por ordenador (DAO). == Visiones generales de la DAO == # J.A. Alonso. [h...'

2015-10-15T06:21:18Z

Página creada con 'En esta página se recogen en enlaces que sirven de documentación al curso de demostración asistida por ordenador (DAO). == Visiones generales de la DAO == # J.A. Alonso. [h...'

Página nueva

En esta página se recogen en enlaces que sirven de documentación al curso de demostración asistida por ordenador (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. 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.
# 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. 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/sadhana/Pdf2009Feb/3.pdf Proof assistants: History, ideas and future]. ''Sadhana'', Vol. 34-1, pp. 3-25, février 2009.
# 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.
# 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.ams.org/notices/200811/tx081101395p.pdf Formal proof: Theory and practice]. ''Notices of the AMS'', Vol. 55, N. 11 (2008) p.1395-1406.
# 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].
# G. Sutcliffe. [http://www.cs.miami.edu/~tptp/OverviewOfATP.html What is automated theorem proving?].
# 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.cs.ru.nl/~freek/pubs/qed2.ps.gz The QED manifesto revisited]. ''Studies in Logic, Grammar and Rhetoric'', Vol. 10(23), pp. 121-133, 2007.

== Referencias sobre Isabelle/HOL ==
# B. Grechuk [http://dream.inf.ed.ac.uk/projects/isabelle/Isabelle_Primer.pdf Isabelle primer for mathematicians].
# T. Nipkow [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/doc/prog-prove.pdf Programming and proving in Isabelle/HOL]. 5 de diciembre de 2013.
# T. Nipkow, M. Wenzel y L.C. Paulson [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/doc/tutorial.pdf A proof assistant for higher-order logic]. Springer-Verlag. 5 de diciembre de 2013.
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL/document.pdf Isabelle/HOL — Higher-Order Logic]. 5 de diciembre de 2013.
# M. Wenzel [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/doc/isar-ref.pdf The Isabelle/Isar Reference Manual]. 5 de diciembre de 2013.
# M. Wenzel [https://www.lri.fr/~wenzel/Isabelle2011-Paris/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 Isabelle2013].

== Lecturas complementarias ==
=== Programación funcional ===
# J.A. Alonso [http://www.cs.us.es/~jalonso/cursos/i1m/temas/2012-13-IM-temas-PF.pdf Temas de "Programación funcional"]. 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.
# M. Lipovača [http://aprendehaskell.es ¡Aprende Haskell por el bien de todos!].

=== Lógica computacional ===
# J.A. Alonso [http://www.cs.us.es/~jalonso/cursos/li/temas/temas-LI-2012-13.pdf Temas de "Lógica informática" (2012-13)]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
# R. Bornat [http://bit.ly/oithic Proof and disproof in formal logic: an introduction for programmers]. Oxford University Press, 2005.
# 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. 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://goo.gl/TMqOo 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 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://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 Tjark Weber. [http://cl-informatik.uibk.ac.at/teaching/ws06/atp/introduction.php Automated Theorem Proving in Isabelle/HOL]. (Univ. de Innsbruck, 2006-07).
# 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).
# Jacques Fleuriot y Paul Jackson. [http://www.inf.ed.ac.uk/teaching/courses/ar/slides/ Automated reasoning]. (Univ. de Edimburgo, 2012-13).
# Thomas Genet [http://www.irisa.fr/celtique/genet/ACF Software formal analysis and design]. (Univ. de Rennes)
# Gerwin Klein. [http://www.cse.unsw.edu.au/~kleing/teaching/thprv-04 Theorem Proving - Principles, Techniques, Applications]. (NICTA, 2004).
# Gerwin Klein. [http://www.cse.unsw.edu.au/~cs4161/index.html Advanced Topics in Software Verification]. (NICTA, 2012).
# Joao Marcos. [http://www.dimap.ufrn.br/~jmarcos/courses/LC/Ementa.htm Lógica computacional: Demonstração assistida e semi-automática de teoremas].(UFRN, 2000).
# Tobias Nipkow. [http://www4.informatik.tu-muenchen.de/~nipkow/semantics/ Semantics of programming languages]. (Univ. de Munich, 2012-13).
# Tobias Nipkow [http://isabelle.in.tum.de/coursematerial/PSV2009-1 Theorem Proving with Isabelle/HOL An Intensive Course].
# 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/SVHOL10 Specification and Verification with Higher-Order Logic].
# Viorel Preoteasa, Ralph-Johan Back y Charmi Panchal. [http://users.abo.fi/vpreotea/isabelle-2012 Introduction to mechanized reasoning with Isabelle/HOL]. (Åbo Akademi University, 2012).
# 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).
# 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).
# Tjark Weber. [http://www.cl.cam.ac.uk/teaching/1011/L21/ Interactive Formal Verification]. (Univ. de Cambridge, 2010-11).

=== Otros cursos ===
# José A. Alonso [http://www.cs.us.es/~jalonso/cursos/li/ 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).
# Yves Bertot, Pierre Casteran, Benjamin Gregoire, Pierre Letouzey y Assia Mahboubi [http://www.di.ens.fr/~zappa/teaching/coq/ecole11 Modelling and verifying algorithms in Coq: an introduction]. (INRIA Paris-Rocquencourt, 14-18 noviembre 2011).
# Pierre Castéran [http://www.labri.fr/perso/casteran/FM/Logique/index.html Logic (Master In Verification)] (Univ. de Burdeos, 2011-12).
# Adam Chlipala [http://stellar.mit.edu/S/course/6/fa11/6.892/ Interactive computer theorem proving]. (MIT, 2012-13).
# Adam Chlipala y Armando Solar Lezama [https://stellar.mit.edu/S/course/6/fa13/6.820/index.html Foundations of program analysis]. (MIT, 2013-14).
# Robby Findler [http://www.eecs.northwestern.edu/~robby/courses/395-495-2013-fall Certified programming with dependent types]. (Northwestern, 2013-14).
# Nuno Gaspar [http://www-sop.inria.fr/members/Nuno.Gaspar/teaching/coq2012.php Verification with the Coq Proof Assistant] (INRIA Sophia Antipolis, 2012-13).
# Carlos Luna y Gustavo Betarte. [https://eva.fing.edu.uy/course/view.php?id=363 Construcción formal de programas en teoría de tipos]. (Univ. de la República, Uruguay, 2013-14).
# Michael Genesereth [http://logic.stanford.edu/classes/cs157/2011/cs157.html Computational Logic] (Univ. de Stanford, 2011-12).
# Ian Hodkinson [http://www.doc.ic.ac.uk/~imh/teaching/140_logic/logic.html Logic] (Imperial College, Londres, 2010-11).
# 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).
# David Pichardie [http://www.irisa.fr/celtique/pichardie/teaching/M2/MDV/ Méthode de vérification] (Universidad de Rennes, 2006-07).
# Michael Winter [Logic in Computer Science] (Brock University, Ontario, Canada, 2010-11).

== Bibliotecas de ejemplos de verificación ==
# [http://afp.sourceforge.net Archive of Formal Proofs].
# [http://www.cs.ru.nl/~freek/100 Formalizing 100 Theorems].
# [http://toccata.lri.fr/gallery Gallery of verified programs].
# [http://www.cs.nott.ac.uk/~lad/research/challenges/ Induction Challenge Problems].
# [http://automatedreasoning.net/ Larry Wos' Notebooks].
# [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 ==
Están en orden cronológico inverso a la fecha de su reseña en [http://www.glc.us.es/~jalonso/vestigium/tag/resena Vestigium]:
# [http://bit.ly/1iZjgqN Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem]. L. Noschinski
# [http://bit.ly/1iJ8uVz A graph library for Isabelle]. ~ L. Noschinski
# [http://bit.ly/I0CU80 Gödel’s incompleteness theorems]. ~ L.C. Paulson
# [http://bit.ly/I0CPRN The hereditarily finite sets]. ~ L.C. Paulson
# [http://bit.ly/HBiIJI Applications of real number theorem proving in PVS]. ~ H. Gottliebsen, R. Hardy, O. Lightfoot y U. Martin
# [http://bit.ly/1awnMLB A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets]. ~ L.C. Paulson
# [http://bit.ly/19lWeYy Verified AIG algorithms in ACL2]. ~ J. Davis y S. Swords
# [http://bit.ly/GAhC00 A formal model and correctness proof for an access control policy framework]. ~ C. Wu, X. Zhang y C. Urban
# [http://bit.ly/16SMvSS The ontological argument in PVS]. ~ J. Rushby
# [http://bit.ly/1dRt9n0 Formalizing Moessner’s theorem and generalizations in Nuprl]. ~ M. Bickford, D. Kozen y A. Silva
# [http://bit.ly/1bSeDNB Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model]. ~ M. Ayala y Y. Santos
# [http://bit.ly/1feFqWE Proof assistant based on didactic considerations]. ~ J. Pais y A Tasistro
# [http://bit.ly/18tHNBi Theory exploration for interactive theorem proving]. ~ M. Johansson
# [http://bit.ly/1b0242s From Tarski to Hilbert]. ~ G. Braun y J. Narboux
# [http://bit.ly/18HaXaR Formal verification of language-based concurrent noninterference]. ~ A. Popescu, J. Hölzl y T. Nipkow
# [http://bit.ly/1aRTQsU A Traffic Alert and Collision Avoidance System(TCAS-II) Resolution Advisory Algorithm]. ~ C. Muñoz, A. Narkawicz y J. Chamberlain
# [http://bit.ly/1dNwhDI Formal verification of cryptographic security proofs]. ~ M. Berg
# [http://bit.ly/17muAUv Polygonal numbers in Mizar]. ~ A. Grabowski
# [http://bit.ly/1hk5z6L A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle]. ~ L.C. Paulson
# [http://bit.ly/1cSL0wE Steps towards verified implementations of HOL Light]. ~ M.O. Myreen, S. Owens y R. Kumar
# [http://bit.ly/16Kbgm0 Generic datatypes à la carte]. ~ S. Keuchel y T. Schrijvers
# [http://bit.ly/1bqJGx4 Proof pearl: A verified bignum implementation in x86-64 machine code]. ~ M.O. Myreen y G. Curello
# [http://bit.ly/142ow2Q Mechanized metatheory for a λ λ-calculus with trust types]. ~ R. Ribeiro, C. Camarão y L. Figueiredo
# [http://bit.ly/15WZBDy Proving soundness of combinatorial Vickrey auctions and generating verified executable code]. ~ M.B. Caminati, M. Kerber, C. Lange y C. Rowat
# [http://bit.ly/198g4n9 A computer-assisted proof of correctness of a marching cubes algorithm]. ~ A.N. Chernikov y J. Xu
# [http://bit.ly/11QA5g7 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
# [http://bit.ly/1cJAXYk The Königsberg bridge problem and the friendship theorem]. ~ W. Li
# [http://bit.ly/13DBK9R Formal verification of a proof procedure for the description logic ALC]. ~ M. Chaabani, M. Mezghiche y M. Strecker
# [http://bit.ly/1ep2ex9 Pratt’s primality certificates]. ~ S. Wimmer y L. Noschinski
# [http://bit.ly/13C95Ci Reasoning about higher-order relational specifications]. ~ Y. Wang, K. Chaudhuri, A. Gacek y G. Nadathur
# [http://bit.ly/18QQLcL Proofs you can believe in – Proving equivalences between Prolog semantics in Coq]. ~ J. Kriener, A. King y S. Blazy
# [http://bit.ly/19uc82J Certified, efficient and sharp univariate Taylor models in Coq]. ~ E. Martin-Dorel, L. Rideau, L. Théry, M. Mayero y I. Paşca
# [http://bit.ly/1c4Rzel Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁]. ~ M. Norrish y B. Huffman
# [http://bit.ly/14b4Akz Program verification based on Kleene algebra in Isabelle/HOL] ~ A. Armstrong, G. Struth y T. Weber
# [http://bit.ly/1aOgRKx Reading an algebra textbook (by translating it to a formal document in the Isabelle/Isar language)]. ~ C. Ballarin
# [http://bit.ly/11HKixj Computational verification of network programs in Coq]. ~ G. Stewart
# [http://www.glc.us.es/~jalonso/vestigium/resena-certifying-homological-algorithms-to-study-biomedical-images Certifying homological algorithms to study biomedical images]. ~ M. Poza
# [http://bit.ly/16Nks9m Formalizing cut elimination of coalgebraic logics in Coq]. ~ H. Tews
# [http://www.glc.us.es/~jalonso/vestigium/resena-the-formalization-of-syntax-based-mathematical-algorithms-using-quotation-and-evaluation/ The formalization of syntax-based mathematical algorithms using quotation and evaluation]. ~ W.M. Farmer
# [http://www.glc.us.es/~jalonso/vestigium/resena-certified-symbolic-manipulation-bivariate-simplicial-polynomials/ Certified symbolic manipulation: Bivariate simplicial polynomials]. ~ L. Lambán, F.J. Martín, J. Rubio y J.L. Ruiz
# [http://www.glc.us.es/~jalonso/vestigium/resena-solveurs-cpfd-verifies-formellement/ Solveurs CP(FD) vérifiés formellement]. ~ C Dubois y A. Gotlieb
# [http://www.glc.us.es/~jalonso/vestigium/resena-formalizing-bounded-increase/ Formalizing bounded increase]. ~ R. Thiemann
# [http://www.glc.us.es/~jalonso/vestigium/resena-formal-mathematics-on-display-a-wiki-for-flyspeck/ Formal mathematics on display: A wiki for Flyspeck]. ~ C. Tankink, C. Kaliszyk, J. Urban y H. Geuvers
# [http://www.glc.us.es/~jalonso/vestigium/resena-theorem-of-three-circles-in-coq Theorem of three circles in Coq]. ~ J. Zsidó
# [http://bit.ly/19fiWAY Certified HLints with Isabelle/HOLCF-Prelude]. ~ J. Breitner, B. Huffman, N. Mitchell y C. Sternagel
# [http://bit.ly/ZfSQrQ Automatic data refinement]. ~ P. Lammich
# [http://bit.ly/18vyjm7 The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups)]. ~ A. Mahboubi
# [http://bit.ly/114oyZV Mechanical verification of SAT refutations with extended resolution]. ~ N. Wetzler, M.J.H. Heule y W.A. Hunt Jr.
# [http://bit.ly/13H0REu Type classes and filters for mathematical analysis in Isabelle/HOL] ~ J. Hölzl, F. Immler y B. Huffman
# [http://bit.ly/10fv8wO Verifying refutations with extended resolution]. ~ M. J. H. Heule, W. A. Hunt, Jr. y N. Wetzler
# [http://bit.ly/10EcFWj A Web interface for Isabelle: The next generation]. ~ C. Lüth y M. Ring
# [http://bit.ly/18P9CSv On the formalization of continuous-time Markov chains in HOL]. ~ L. Liu, O. Hasan y S. Tahar
# [http://bit.ly/17H2mqy Formalizing Turing machines]. ~ A. Asperti y W. Ricciotti
# [http://bit.ly/YwuCeL Light-weight containers for Isabelle: efficient, extensible, nestable]. ~ A. Lochbihler
# [http://bit.ly/10XLrRA Graph theory]. ~ L. Noschinski
# [http://bit.ly/19kPEP4 A machine-checked proof of the odd order theorem]. ~ G. Gonthier et als.
# [http://goo.gl/LdihL A constructive theory of regular languages in Coq]. ~ C. Doczkal, J.O. Kaiser y G. Smolka
# [http://goo.gl/gwcwL A formal proof of Kruskal’s tree theorem in Isabelle/HOL]. ~ C. Sternagel
# [http://goo.gl/CUF3e Formalizing Knuth-Bendix orders and Knuth-Bendix completion]. ~ C. Sternagel y R. Thiemann
# [http://goo.gl/9JAfX Developing an auction theory toolbox]. ~ C. Lange, C. Rowat, W. Windsteiger y M. Kerber
# [http://goo.gl/6OfmQ Formalization of incremental simplex algorithm by stepwise refinement]. ~ M. Spasić y F. Marić
# [http://goo.gl/Guxky Coinductive pearl: Modular first-order logic completeness]. ~ J.C. Blanchette, A. Popescu y D. Traytel
# [http://goo.gl/HUOl8 A fully verified executable LTL model checker]. ~ J. Esparza et als.
# [http://goo.gl/RV54S ForMaRE - formal mathematical reasoning in economics]. ~ M. Kerber, C. Lange y C. Rowat.
# [http://goo.gl/Y7sIq AI over large formal knowledge bases: The first decade]. ~ J. Urban.
# [http://goo.gl/vvqNg Formalization of real analysis: A survey of proof assistants and libraries]. ~ S. Boldo, C. Lelay y G. Melquiond.
# [http://goo.gl/bEFYa Data refinement in Isabelle/HOL]. ~ F. Haftmann, A. Krauss, O. Kunčar y T. Nipkow
# [http://goo.gl/xTyvE Formalizing the confluence of orthogonal rewriting systems]. ~ A.C. Rocha y M. Ayala.
# [http://goo.gl/zCYHj Formalization of the complex number theory in HOL4]. ~ Z. Shi et als.
# [http://goo.gl/kM0dI Programming and reasonning with PowerLists in Coq]. ~ F. Loulergue y V. Niculescu
# [http://goo.gl/KkU6s A hierarchy of mathematical structures in ACL2]. ~ J. Heras, F.J. Martín y V. Pascual.
# [http://www.inf.kcl.ac.uk/staff/urbanc/Publications/tm.pdf Mechanising Turing Machines and Computability Theory in Isabelle/HOL] ~ J. Xu, X. Zhang y C. Urban

← Revisión anterior		Revisión del 17:22 8 feb 2022
Línea 1:		Línea 1:
−	En esta página se recogen en enlaces que sirven de documentación al curso de demostración asistida por ordenador (DAO).	+	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 [https://www.glc.us.es/~jalonso/RA2019/index.php/Documentaci%C3%B3n curso 2019-20].

	== Visiones generales de la DAO ==		== Visiones generales de la DAO ==

@@ Línea 23: / Línea 23: @@
 # B. Grechuk [http://dream.inf.ed.ac.uk/projects/isabelle/Isabelle_Primer.pdf Isabelle primer for mathematicians].
 # T. Nipkow [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2015/doc/prog-prove.pdf Programming and proving in Isabelle/HOL]. 25 de mayo de 2015
-# T. Nipkow, M. Wenzel y L.C. Paulson [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2015/doc/tutorial.pdf A proof assistant for higher-order logic]. Springer-Verlag.
+# T. Nipkow, M. Wenzel y L.C. Paulson [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2015/doc/tutorial.pdf A proof assistant for higher-order logic]. Springer-Verlag. 25 de mayo de 2015
-# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL/document.pdf Isabelle/HOL — Higher-Order Logic]. 5 de diciembre de 2013.
+# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL/document.pdf Isabelle/HOL — Higher-Order Logic]. 25 de mayo de 2015
-# M. Wenzel [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2015/doc/isar-ref.pdf The Isabelle/Isar Reference Manual]. 5 de diciembre de 2013.
+# M. Wenzel [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2015/doc/isar-ref.pdf The Isabelle/Isar Reference Manual]. 25 de mayo de 2015
 # M. Wenzel [https://www.lri.fr/~wenzel/Isabelle2011-Paris/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 Isabelle2013].
+# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/documentation.html Tutorials and manuals for Isabelle].
 == Lecturas complementarias ==

@@ Línea 22: / Línea 22: @@
 == Referencias sobre Isabelle/HOL ==
 # B. Grechuk [http://dream.inf.ed.ac.uk/projects/isabelle/Isabelle_Primer.pdf Isabelle primer for mathematicians].
-# T. Nipkow [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/doc/prog-prove.pdf Programming and proving in Isabelle/HOL]. 5 de diciembre de 2013.
+# T. Nipkow [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2015/doc/prog-prove.pdf Programming and proving in Isabelle/HOL]. 25 de mayo de 2015
 # T. Nipkow, M. Wenzel y L.C. Paulson [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/doc/tutorial.pdf A proof assistant for higher-order logic]. Springer-Verlag. 5 de diciembre de   2013.
 # [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL/document.pdf Isabelle/HOL — Higher-Order Logic]. 5 de diciembre de 2013.