Teaching plan for the course unit



Close imatge de maquetació




General information


Course unit name: Theory of Demonstration and Automatic Demonstration

Course unit code: 569076

Academic year: 2021-2022

Coordinator: Joost Johannes Joosten

Department: Department of Philosophy

Credits: 5

Single program: S

More information enllaç



Estimated learning time

Total number of hours 125


Face-to-face and/or online activities



-  Lecture




Supervised project


Independent learning




Competences to be gained during study


To be able to provide formal proofs in various proof systems for both propositional and predicate logic, including

  1. Natural deduction;
  2. Sequent calculus;
  3. 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;

finitary versus non-finitary;

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.



Reading and study resources

Consulteu la disponibilitat a CERCABIB


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.