Teaching plan for the course unit

 

 

Close imatge de maquetació

 

Print

 

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

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

  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;
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.

 

 

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 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.