Razonamiento automático (2017-18) - Contribuciones del usuario [es]

Documentación

2017-10-16T08:06:48Z

WikiSysop: /* Visiones generales de la DAO */

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/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/article/fulltext/sadh/034/01/0003-0025 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.
# J. Gross [https://blogs.ams.org/mathgradblog/2017/10/15/machine-checked-proof Machine-checked proof]. ''AMS Notices'', 15 de octubre de 2017.
# 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://mizar.org/trybulec65/8.pdf 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 [https://isabelle.in.tum.de/doc/prog-prove.pdf Programming and proving in Isabelle/HOL].
# T. Nipkow, M. Wenzel y L.C. Paulson [http://isabelle.in.tum.de/doc/tutorial.pdf A proof assistant for higher-order logic].
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL/document.pdf Isabelle/HOL — Higher-Order Logic].
# M. Wenzel [http://isabelle.in.tum.de/doc/isar-ref.pdf The Isabelle/Isar Reference Manual].
# M. Wenzel [http://typessummerschool07.cs.unibo.it/courses/wenzel-isar-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 Isabelle].

== Lecturas complementarias ==
=== Programación funcional ===
# J.A. Alonso [https://www.cs.us.es/~jalonso/cursos/i1m-16/temas/2016-17-IM-temas-PF.pdf Temas de "Programación funcional"]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2016.
# 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 [https://www.cs.us.es/~jalonso/cursos/li-15/temas/temas-LI-2015-16.pdf 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 [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://bit.ly/2e8dFEm 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).
# Jasmin Blanchette, Mathias Fleury y Daniel Wand [http://people.mpi-inf.mpg.de/~jblanche/cswi/ss2015/ Concrete semantics with Isabelle/HOL]. (Univ. del Sarre, 2015-16).
# 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. [http://www.inf.ed.ac.uk/teaching/courses/ar Automated reasoning]. (Univ. de Edimburgo, 2016-17).
# 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://www21.in.tum.de/teaching/semantik/WS1617/ 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/de/teaching/SVHOL14/ Specification and Verification with Higher-Order Logic].
# 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).
# 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).
# 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).

== 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://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

Documentación

2017-10-16T08:06:08Z

WikiSysop: /* Visiones generales de la DAO */

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/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/article/fulltext/sadh/034/01/0003-0025 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.
# J. Gross [https://blogs.ams.org/mathgradblog/2017/10/15/machine-checked-proof Machine-checked proof]. ''AMS Notices', 15 de octubre de 2017.
# 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://mizar.org/trybulec65/8.pdf 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 [https://isabelle.in.tum.de/doc/prog-prove.pdf Programming and proving in Isabelle/HOL].
# T. Nipkow, M. Wenzel y L.C. Paulson [http://isabelle.in.tum.de/doc/tutorial.pdf A proof assistant for higher-order logic].
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL/document.pdf Isabelle/HOL — Higher-Order Logic].
# M. Wenzel [http://isabelle.in.tum.de/doc/isar-ref.pdf The Isabelle/Isar Reference Manual].
# M. Wenzel [http://typessummerschool07.cs.unibo.it/courses/wenzel-isar-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 Isabelle].

== Lecturas complementarias ==
=== Programación funcional ===
# J.A. Alonso [https://www.cs.us.es/~jalonso/cursos/i1m-16/temas/2016-17-IM-temas-PF.pdf Temas de "Programación funcional"]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2016.
# 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 [https://www.cs.us.es/~jalonso/cursos/li-15/temas/temas-LI-2015-16.pdf 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 [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://bit.ly/2e8dFEm 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).
# Jasmin Blanchette, Mathias Fleury y Daniel Wand [http://people.mpi-inf.mpg.de/~jblanche/cswi/ss2015/ Concrete semantics with Isabelle/HOL]. (Univ. del Sarre, 2015-16).
# 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. [http://www.inf.ed.ac.uk/teaching/courses/ar Automated reasoning]. (Univ. de Edimburgo, 2016-17).
# 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://www21.in.tum.de/teaching/semantik/WS1617/ 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/de/teaching/SVHOL14/ Specification and Verification with Higher-Order Logic].
# 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).
# 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).
# 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).

== 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://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

Documentación

2017-10-16T08:05:41Z

WikiSysop: /* Visiones generales de la DAO */

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/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/article/fulltext/sadh/034/01/0003-0025 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.
# Gross, J [https://blogs.ams.org/mathgradblog/2017/10/15/machine-checked-proof Machine-checked proof]. ''AMS Notices', 15 de octubre de 2017.
# 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://mizar.org/trybulec65/8.pdf 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 [https://isabelle.in.tum.de/doc/prog-prove.pdf Programming and proving in Isabelle/HOL].
# T. Nipkow, M. Wenzel y L.C. Paulson [http://isabelle.in.tum.de/doc/tutorial.pdf A proof assistant for higher-order logic].
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL/document.pdf Isabelle/HOL — Higher-Order Logic].
# M. Wenzel [http://isabelle.in.tum.de/doc/isar-ref.pdf The Isabelle/Isar Reference Manual].
# M. Wenzel [http://typessummerschool07.cs.unibo.it/courses/wenzel-isar-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 Isabelle].

== Lecturas complementarias ==
=== Programación funcional ===
# J.A. Alonso [https://www.cs.us.es/~jalonso/cursos/i1m-16/temas/2016-17-IM-temas-PF.pdf Temas de "Programación funcional"]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2016.
# 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 [https://www.cs.us.es/~jalonso/cursos/li-15/temas/temas-LI-2015-16.pdf 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 [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://bit.ly/2e8dFEm 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).
# Jasmin Blanchette, Mathias Fleury y Daniel Wand [http://people.mpi-inf.mpg.de/~jblanche/cswi/ss2015/ Concrete semantics with Isabelle/HOL]. (Univ. del Sarre, 2015-16).
# 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. [http://www.inf.ed.ac.uk/teaching/courses/ar Automated reasoning]. (Univ. de Edimburgo, 2016-17).
# 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://www21.in.tum.de/teaching/semantik/WS1617/ 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/de/teaching/SVHOL14/ Specification and Verification with Higher-Order Logic].
# 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).
# 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).
# 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).

== 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://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

MediaWiki:Sidebar

2017-10-14T16:39:17Z

WikiSysop:

* navigation
** mainpage|mainpage-description
** http://www.cs.us.es/~jalonso/cursos/m-ra-17/temas.php|Temas
** Ejercicios|Ejercicios
** Documentación|Documentación
** http://www.glc.us.es/~jalonso/vestigium/tag/ra2017|Diario
** https://twitter.com/search?f=tweets&q=%23RA2017%20from:Jose_A_Alonso|Twitter
** recentchanges-url|recentchanges
* SEARCH
* TOOLBOX
* LANGUAGES

Sistemas

2017-09-09T06:39:27Z

WikiSysop: Página creada con '== Sistemas utilizados en ''Razonamiento automático (2017-18)'' == En esta página se irá escribiendo enlaces a los sistemas utilizados en el curso # [http://www.cl.cam.ac.uk...'

== Sistemas utilizados en ''Razonamiento automático (2017-18)'' ==

En esta página se irá escribiendo enlaces a los sistemas utilizados en el curso
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html Isabelle/HOL].
# [http://www.glc.us.es/apli2 APLI2 (APLIcación de Ayuda Para Lógica Informática)].

Documentación

2017-09-09T06:38:15Z

WikiSysop: 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/NWk7...'

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/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/article/fulltext/sadh/034/01/0003-0025 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://mizar.org/trybulec65/8.pdf 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 [https://isabelle.in.tum.de/doc/prog-prove.pdf Programming and proving in Isabelle/HOL].
# T. Nipkow, M. Wenzel y L.C. Paulson [http://isabelle.in.tum.de/doc/tutorial.pdf A proof assistant for higher-order logic].
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL/document.pdf Isabelle/HOL — Higher-Order Logic].
# M. Wenzel [http://isabelle.in.tum.de/doc/isar-ref.pdf The Isabelle/Isar Reference Manual].
# M. Wenzel [http://typessummerschool07.cs.unibo.it/courses/wenzel-isar-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 Isabelle].

== Lecturas complementarias ==
=== Programación funcional ===
# J.A. Alonso [https://www.cs.us.es/~jalonso/cursos/i1m-16/temas/2016-17-IM-temas-PF.pdf Temas de "Programación funcional"]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2016.
# 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 [https://www.cs.us.es/~jalonso/cursos/li-15/temas/temas-LI-2015-16.pdf 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 [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://bit.ly/2e8dFEm 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).
# Jasmin Blanchette, Mathias Fleury y Daniel Wand [http://people.mpi-inf.mpg.de/~jblanche/cswi/ss2015/ Concrete semantics with Isabelle/HOL]. (Univ. del Sarre, 2015-16).
# 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. [http://www.inf.ed.ac.uk/teaching/courses/ar Automated reasoning]. (Univ. de Edimburgo, 2016-17).
# 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://www21.in.tum.de/teaching/semantik/WS1617/ 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/de/teaching/SVHOL14/ Specification and Verification with Higher-Order Logic].
# 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).
# 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).
# 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).

== 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://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

Ejercicios

2017-09-09T06:37:46Z

WikiSysop: Página creada con '== Relaciones de ejercicios == === Relaciones de ejercicios propuestos === En esta sección se publicarán las relaciones de ejercicios. Las soluciones se escriben de forma co...'

== Relaciones de ejercicios ==

=== Relaciones de ejercicios propuestos ===

En esta sección se publicarán las relaciones de ejercicios. Las soluciones se escriben de forma colaborativa por los alumnos del curso y no deben tomarse como definitivas.

Temas

2017-09-09T06:37:12Z

WikiSysop: Página creada con '== Temas de ''Razonamiento automático (2017-18)'' == En esta página se irán publicando los temas conforme se vayan estudiando.'

== Temas de ''Razonamiento automático (2017-18)'' ==

En esta página se irán publicando los temas conforme se vayan estudiando.

Razonamiento automático (2017-18)

2017-09-09T06:35:46Z

WikiSysop: Página creada con '== Razonamiento automático (2017-18) == Este sitio contiene materiales del curso ''Razonamiento automático'' del [http://master.cs.us.es/Máster_Universitario_en_Lógica,_Comp...'

== Razonamiento automático (2017-18) ==
Este sitio contiene materiales del curso ''Razonamiento automático'' del [http://master.cs.us.es/Máster_Universitario_en_Lógica,_Computación_e_Inteligencia_Artificial Máster Universitario en Lógica, Computación e Inteligencia Artificial] de la [http://www.us.es Universidad de Sevilla].

== Material para el curso ==
* [[Temas]]: Teorías de los temas.
* [[Ejercicios]]: Relaciones de ejercicios.
* [[Documentación]]: Lecturas recomendadas.
* [[Sistemas]]: Sistemas utilizados.
* [http://www.glc.us.es/~jalonso/vestigium/tag/ra2017 Diario]: Descripción diaria de las clases.
* [https://github.com/jaalonso/RA20117 GitHub]: Curso en GitHub.

MediaWiki:Mainpage

2017-09-09T06:34:41Z

WikiSysop: Página creada con 'Razonamiento automático (2017-18)'

Razonamiento automático (2017-18)

MediaWiki:Sidebar

2017-09-09T06:33:55Z