General information 
Course unit name: Theory of Demonstration and Automatic Demonstration
Course unit code: 569076
Academic year: 20212022
Coordinator: Joost Johannes Joosten
Department: Department of Philosophy
Credits: 5
Single program: S
Estimated learning time 
Total number of hours 125 
Facetoface and/or online activities 
42 
 Lecture 
Facetoface 
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
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.
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.

Teaching blocks 
1. Formal proof systems
* Rules;
Axioms;
finitary versus nonfinitary;
omegarule;
2. Ordinal analysis
* Foundations of mathematics;
Consistency proofs;
3. Automated reasoning in propositional logic
*
 Basic notions;
 The method of resolution;
 The method of Davis and Putnam.
4. Automated reasoning in predicate logic
*
 Skolem forms;
 Semantic trees/tableaux;
 Herbrand’s method;
 The Unification Algorithm;
 The method of resolution;
 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. 
Official assessment of learning outcomes 
The final grade is determined by (A) Weekly homework questions; (40 %) (B) Midterm takehome 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 twoandahalf of the five credits.
Examinationbased 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
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 textbooks that deal with matters of this course. We will announce what material shall eventually be used apart from the handouts. 
M. BenAri, "Mathematical logic for computer science", thrird edition, Springer, 2012.