Lecture Series on Proof Tools (Wintersemester 2002)
Schedule
- Week 1
-
Introduction, Natural Deduction for First Order Intuitionistic
Logic.
- Week 2
-
Sequent Calculus for Classical First Order Logic,
difference between Intuitionistic and Classical Logic.
- Week 3
-
Simply Typed Lambda Calculus, Higher Order Logic,
Natural Deduction and Sequent Calculus for Higher Order Logic,
Higher Order Logic as Meta-Logic.
Slides
Exercises
- Week 2, November 2nd 2001
-
Exercises in
ps-format
and in
pdf-format
.
- November 23d, 2001
-
Exercises in
ps-format
and in
pdf-format
.
- Feb 1st, 2002
-
Exercises in
ps-format
and in
pdf-format
.
Isabelle
-
Homepage of
Isabelle
.
-
Isabelle has to be started by typing
/HG/opt/provers/Isabelle99-2/Isabelle99-2/bin/isabelle -I HOL
(Better make a shell-script of this.)