Introduction to Computational Logic

Videos of Lectures 2022

1. April 13, Getting Started
2. April 20, April 22, Getting Started
3. April 27 (slides), April 29, Basic Computational Type Theory, Propositions as Types
4. May 4, May 6, Propositions as Types, Conversion Rule, Propositional Equality
5. May 11, May 13, Leibniz Equality, Inductive Eliminators
6. May 18, May 20, Existential Quantification, General Remarks
7. May 25, May 27, Certifying Functions, Sum and Sigma Types, Bijection Types, Decision Types
8. June 1, June 3, Option Types, Finite Types, Extensionality
9. June 8, June 10, Numbers, Euclidean Division
10. June 17, Euclidean Division, Least Witnesses (recordings of June 15 and of first half of June 17 lost)
11. June 22, June 24, Lists, Compiler Verification, Least Witnesses
12. June 29, July 1, Discriminating Elements, Existential Witnesses
13. July 6, July 8, Propositional Deduction Systems
14. July 13 (slides), July 15, Hilbert systems, boolean and Heyting evaluation, refutation systems, certifying solver, decidability
15. July 20, Refutation systems, round up

Videos of lectures from 2021

1. April 14, April 16, Getting Started
2. April 21, April 23, Basic Computational Type Theory, Propositions as Types
3. April 28, April 30, Propositions as Types, Conversion Rule, Leibniz Equality
4. May 5, May 7, 202, Inductive Eliminators, Cantor Pairing
5. May 12, May 14, Existential Quantification, Executive Summary
6. May 19, May 21, Informative Types, Decision Types, Extensionality
7. May 26, May 28, Excluded Middle, Numbers
8. June 2, June 4, Euclidean Division, Least Witnesses
9. June 9, June 11, 2021, Size Recursion, Procedural Specifications, Step Indexing
10. June 16, June 18, 2021, Lists, Expression Compiler
11. June 23, June 25, Indexed Numerals, Binary derivation system for comparisons
12. June 30, July 2, Derivations systems for GCDs and regular expressions
13. July 7, July 9, ND and Hilbert systems, intuitionistic and classic
14. July 14, July 16, 2021, Heyting interpretation, boolean interpretation, certifying boolean solver, inductive equality
15. July 21, Last lecture, review and outlook (finite types and higher-order recursion)

Supplementary videos

• Getting Started with Coq (April 15, 2021)
• 10 Proofs of Leibniz Symmetry (April 6, 2021)
• Exercise Sheet 4 Presentation (May 17, 2021)
• Exercise Sheet 4 Discussion (May 19, 2021)
• Exercise Sheet 7 Discussion (June 07, 2021)
• Videos explaining how to write proofs (diagrams and Coq) (by Chad E. Brown, 2014 and 2015)