## Course: Exercises in Information Sciences II (Theorem Proving)

Every Wednesday from 10:40 to 12:10

Rooms: 理学部3号館504室 or 共通講義棟3号館408室

**[Theme]** In a course of mathematical logic, a student performs pen-and-paper formal proofs by means of logical derivations. How does a student know that her formal proof is correct? complete? Alternatively, she can use a software/tool such as a proof assistant. The advantage of using a proof assistant in the class is to, first, check the correctness of a proof, and, second, assist the student in writing a formal proof where no step is omitted, the logic is explicit and the proof method is clearly stated.

**[Objective]** In this class, we:

- learn how to write formal proofs using the proof assistant Isabelle/HOL (https://isabelle.in.tum.de/).
- study and practice various proving techniques (e.g. natural deduction, induction, etc.).

#### Course materials

- 2018.10.03, room 504: Course overview: Why theorem proving is vital? slides, Isabelle/HOL symbols
- 2018.10.10, room 504: Propositional logic (I) slides
- 2018.10.17, room 504: Propositional logic (II) slides, mt rules
- 2018.10.24, room 504: Propositional logic (III) slides
- 2018.10.31, room 504: Exercises exercises
- 2018.11.07, room 504: Predicate logic (I) slides
- 2018.11.14, room 504: Predicate logic (II) slides
- 2018.11.21, room 504: Exercises exercises
- 2018.11.28, room 504: Exercises (continued) Examples of script style proofs
- 2018.12.05, room 504: Mathematical induction - Type nat slides
- 2018.12.12, room 504: Mathematical induction - Type nat (II) slides
- 2018.12.19, room 504: Recursive functions slides
- 2018.12.26, room 504: Structural induction - Type list slides
- 2019.01.16, room 504 or 505: Structural induction - Type list (II)slides
- 2019.01.23, room 504: Final problem

#### Lecturer

Fadoua Ghourabi

Contact: ghourabi "dot" fadoua "at" ocha "dot" ac "dot" jp

Office: 人間文化創成科学研究科・全学共用研究棟 603室

For questions, students can visit my office on Monday from 16:00 to 18:00

This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.