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.).
- 2016.10.05, room 504: Course overview: Why theorem proving is vital? slides, examples
- 2016.10.12, room 504: Propositional logic I (propositions, introduction and elimination rules for logical and double negation). slides, names.thy, quiz+solutions
- 2016.10.19, room 504: Propositional logic II (introduction and elimination rules for implies, disjunction). slides (updated), quiz+solution
- 2016.10.26, room 504:Propositional logic III (introduction and elimination rules for negation, exercises with Isabelle/HOL). slides (updated), examples.
- 2016.11.02, room 504: Practice with Isabelle/HOL. List of rules, exercises, solutions.
- 2016.11.09, room 504: Predicate logic I (terms, formulas, substitution). slides (updated), examples, quiz+solution
- 2016.11.16, room 504: Predicate logic II (natural deduction). slides, examples, quiz+solution
- 2016.11.23, room 504: Practice with Isabelle/HOL. List of rules, exercises, solutions
- 2016.11.30, room 504: Elementary set theory. lecture(until section 4), quiz+solutions
- 2016.12.07, room 504: Elementary set theory, substitution, simplification in Isabelle. lecture
- 2016.12.14, room 504: Base types in Isabelle, proof by induction. slides, quiz+solutions
- 2016.12.21, room 504: Recursive functions. slides
- 2017.01.12, room 504: Lists. slides, Quiz+solutions
- 2017.01.18, room 504: Practice with Isabelle. exercises, notes on exercise 2
- 2017.01.25, room 504: Practice with Isabelle.
- 2017.02.01, room 504: Practice with Isabelle. solutions
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.