En esta página se recopilan cursos de razonamiento automático y demostración asistida por ordenador que sirven de referencia al curso Razonamiento automático de la Universidad de Sevilla.

Está ordenada por países y universidades.

• Computer-supported modeling and reasoning. ~ Jan-Georg Smaus.

• Concrete Semantics with Isabelle/HOL (Summer semester 2015) ~ Jasmin Blanchette, Mathias Fleury y Daniel Wand.
• Introduction to computational logic (Summer Semester 2018) ~ Gert Smolka
• Introduction to computational logic (Summer Semester 2019) ~ Gert Smolka

• Specification and verification with higher-order logic. ~ Arnd Poetzsch-Heffter.

• Introduction to the Isabelle proof assistant. ~ C. Ballarin.
• Introduction to the Isabelle proof assistant. ~ C. Ballarin y G. Klein.
• Semantics of programming languages. ~ Tobias Nipkow.
• Theorem proving with Isabelle/HOL: An intensive course. ~ Tobias Nipkow.

• Advanced topics in software verification. ~ Gerwin Klein.
• Theorem proving: Principles, techniques, applications. ~ Gerwin Klein.

• Automated theorem proving in Isabelle/HOL. ~ C. Ballarin y T. Weber.
• Automatic deduction. ~ C. Ballarin.
• Experiments in verification: Introduction to Isabelle/HOL. ~ Christian Sternagel
• Interactive theorem proving using Isabelle/HOL. ~ Christian Sternagel.
• Machine learning for theorem proving. ~ C. Kaliszyk

• Lógica computacional: Demonstração assistida e semi-automática de teoremas. ~ Joao Marcos.

• Computer-aided reasoning for software engineering. ~ Vijay Ganesh.
• Logic and computation. ~ Prabhakar Ragde.

• Automated reasoning (2013-14). ~ J. Fleuriot y P. Jackson.
• Automated reasoning (2016-17). ~ J. Fleuriot y P. Jackson.

• Data structures and functional programming. ~ Michael Clarkson.

• Logic and formal verification. ~ J. Avigad.
• Logic and proof (Release 0.1). ~ J. Avigad, R.Y. Lewis, F. van Doorn

• Interactive computer theorem proving. ~ A. Chlipala.
• Formal reasoning about programs. ~ A. Chlipala.

• Formal methods: specification, verification, and synthesis. ~ S.A. Seshia.

• Practical theorem proving with Isabelle/Isar. ~ Jeremy G. Siek.
• Theorem proving in Isabelle. ~ Jeremy G. Siek.

• Logic and computation. ~ R. Pucella.

• Software foundations. ~ B.C. Pierce et als.
• Software foundations. Vol. 1: Logical foundations. ~ B.C. Pierce et als.

• Automated logical reasoning. ~ I. Dillig.
• SAT solving and theorem proving. ~ W.A. Hunt, Jr.

• Computer-aided reasoning for software. ~ E. Torlak

• Introduction à l’assistant de preuve Coq. ~ R. Affeldt

• Coq Winter School 2017.
• Cours vidéo de Coq. ~ Y. Bertot.
• Preuves assistées par ordinateur à l’aide de Coq. ~ Y. Bertot.

• Analyse et conception formelles. ~ T. Genet.
• Software formal analysis and design. ~ T. Genet.

• Exercises in Information Sciences II (Theorem Proving). ~ F. Ghourabi

• Interactive formal verification. ~ Larry Paulson.
• Interactive formal verification. ~ Tjark Weber.

• Advanced formal methods. ~ M. Dam.

• Synthesis, analysis, and verification. ~ E. Kneuss, V. Kunčak.

• Computer-supported modeling and reasoning. ~ A.D. Brucker, D. Basin, J.G. Smaus y B. Wolff.