Teaching plan for the course unit

 General information

Course unit name: Theory of Demonstration and Automatic Demonstration

Course unit code: 569076

Coordinator: Joost Johannes Joosten

Department: Department of Philosophy

Credits: 5

Single program: S

 Estimated learning time Total number of hours 125

 Face-to-face and/or online activities 42
 -  Lecture Face-to-face 42
 Supervised project 18
 Independent learning 65

 Competences to be gained during study

 To be able to provide formal proofs in various proof systems for both propositional and predicate logic, including Natural deduction; Sequent calculus; Resolution;To be able to read state of art literature on proof-systems;To understand the correctness of the above mentioned proof systems;To understand the applications of proof theory to ordinal analysis and its repercussions on the foundations of mathematics;To be able to write rudimentary prolog code;

 Learning objectives
 Referring to knowledge The main objective of this course is to obtain a thorough understanding of formal proof systems and their applications in mathematics and computer science. The student will get exposed to the theory but also be required to make formal derivations him/herself. By the end of the course we shall see how reasoning/theorem proving can be automated using PROLOG.We shall reflect on how proof theory provides us with insights about formalized epistemic processes when reasoning about mathematics (and possibly other fields). In particular we shall see how proof theory helps us understand the boundaries of such processes.   Referring to abilities, skills To be able to reason within different kind of formal proof systems like Natural Deduction, Sequent Calculi and Frege/Hilbert Systems. To normalize proofs and retrieve constructive information from such normalised proofs. To solve problems in logic programming.

 Teaching blocks

1. Formal proof systems

*  Rules;
Axioms;

finitary versus non-finitary;
omega-rule;

2. Ordinal analysis

*  Foundations of mathematics;
Consistency proofs;

3. Automated reasoning in propositional logic

*

1. Basic notions;
2. The method of resolution;
3. The method of Davis and Putnam.

4. Automated reasoning in predicate logic

*

1. Skolem forms;
2. Semantic trees/tableaux;
3. Herbrand’s method;
4. The Unification Algorithm;
5. The method of resolution;
6. The PROLOG programming language.

 Teaching methods and general organization

 In the course we shall first provide a historically based overview of the main philosophical questions that lead to the discipline of proof theory. Next we shall see how epistemological processes can be formalized leading to the notions of formal proof and formal proof systems. We do this by lectures and historical examples. The proof systems will be examplified using numerous exercises that have to be handed in on a weekly basis.At first our domain of discourse will be mainly propositional logic to readily switch to predicate logic.

 Official assessment of learning outcomes

 The final grade is determined by (A) Weekly homework questions; (40 %) (B) Midterm take-home exam; (30 %) (C) Final Exam; (30 %). Of these parts Item (A) will be spread out over the whole duration of the course and Item (B) will take place around after two-and-a-half of the five credits.   Examination-based assessment The avaluació única consists of a final exam over all the material discussed in class together with a set of homework exercises.

Book

Uwe Shöning, Logic for Computer Scientists;
C. L. Chang and R.C.T. Lee, Symbolic Logic and Mechanical Theorem Proving;
A. Troelstra and van D. van Dalen, Constructivism in Mathematics;
A. Troelstra, Proof theory.

 These are standard text-books that deal with matters of this course. We will announce what material shall eventually be used apart from the hand-outs.

M. Ben-Ari, "Mathematical logic for computer science", thrird edition, Springer, 2012.