Fte263 / 582418 Proof Theory and Proof Search (3 cu)
General information
- Lectures: PhD Sara
Negri 20.1.-24.2. and 9.3.-6.4. Tue 10-12 Main Building Hall 15.
- Exercises: Raul
Hakli 27.1.-24.2. and 9.3.-30.3. Tue 13-15 Main Building Aud X.
Course description
The course gives a concise introduction to the central methods and
results of structural proof theory. Special emphasis is given to the
design of logical calculi supporting proof-search. The course includes
exercise and demo sessions with the use of an interactive proof-editor
for sequent calculus.
Prerequisites
Expected background is an introductory course in logic.
Course literature
"Structural Proof Theory",
Sara Negri and Jan von Plato, Cambridge U.P. 2001.
Exercises
Additional material and solutions to the exercises
Additional material and solutions to the exercises can be found in the
course folders in the Philosophica library at the Department of
Philosophy (location: 3rd floor of Siltavuorenpenger 20 A) and room
A412 at the Department
of Computer Science (location: 4th floor of Teollisuuskatu 23). Some
of the solutions are available in electronic form here: Solutions 1, 2,
3,
4 (Corrected March 30),
5,
6,
7,
8.
Please let us know if you find any errors in the solutions.
Exam
The course results are available on the bulletin boards now.
There will be another exam on Tuesday, May 25, 10-12 in Hall 15.
The course exam was held on Tuesday April 6, 10-12 in Hall 15
of the Main Building. The exam covers the following parts of the course book:
- Chapter 1: All
- Chapter 2: This chapter is optional (useful reading but not necessary
for the exam)
- Chapter 3: All except 3.3
- Chapter 4: All except 4.3 (b) which is optional and 4.4. Note that
only the first three lines of page 80 belong to 4.3 (b) so Theorem
4.3.8 is included in the exam.
- Chapter 6: All except 6.5 which is optional and 6.6 (d), (e)
- Handouts:
- Hilbert's last problem (by Sara Negri and Jan von Plato, either
in Finnish or in English)
- Propositional modal logic (by M. Fitting and R. Mendelsohn, in First Order Modal Logic, Synthese Library 277)
- A uniform Gentzen approach to the proof theory of modal logic (by Sara Negri)
Links
-
Proof Theory Forum
- Additional
exercises for self-study
- PESCA - a Proof
Editor for Sequent Calculus (requires Haskell)
- ProEd Proof
Editor (in Finnish, but the links ProEd-1.01.tar.gz and ProEd101.zip are
for downloading the software) (requires Java)
raul.hakli@helsinki.fi
Last updated May 17, 2004