The SEMHOL Course:
Semantics of Classical Higher-Order Logic (SEMHOL)
Chad E. Brown
General Course Information
| Program of Studies: | Master Program Computer Science | |
| Name of the module: | Semantics of Classical Higher-Order Logic | |
| Abbreviation: | SEMHOL | |
| Subtitle: | ||
| Modules: | Lecture h (weekly) 2 / Tutorial h (weekly) 2 | |
| Responsible lecturer: | Chad E Brown | |
| Language: | English | |
| Entrance requirements: | Lecture: Introduction to Computational Logic. | |
| Aims / Competence to developed: | Basic overview on the latest developments in the area | |
| Content: | simply typed λ-calculus, propositions, extensionality, calculi, | |
| applicative structures, models, independence | ||
| Used Media: | Blackboard and Computer | |
| Literature: | A commented reading list can be found here. The two main publications | |
| addressed in the lecture are: | ||
| (1) C. Brown, Automated Reasoning in Higher-Order Logic | ||
| (2) C. Benzmüller, C. Brown, and M. Kohlhase, | ||
| Higher Order Semantics and Extensionality. Journal of Symbolic Logic. | ||
| (2004) 69(4):1027-1088. JSTOR |
Exercises/Exam/Grading
Every week or two, students will be assigned exercises. These exercises will be turned in and graded. Part of the point of the exercises will be for the students to work through details omitted in the class, and part of the point will be to apply the ideas presented in class to examples. The exercises will account for 50% of the final grade.
There will be two exams: A midterm exam in December and a final exam at the end of the course. The midterm exam will account for 20% of the final grade and the final exam will acount for 30% of the final grade.
In Summary, the grades will be determined as follows:
50% - Exercises
20% - Midterm Exam
30% - Final Exam
Exercise Sheet
The following are the first two exercise sheets from the Winter 2006-2007 course.
Exercise Sheet 1 (50 Points) Solutions
Exercise Sheet 2 (50 Points) Solutions
Lectures
The following is an outline of the topics we will consider:
Simple Types
Standard and non-standard frames
Typed λ-calculus
Evaluations as Set-Theoretic Semantics of Typed λ-calculus
Logical Constants: HOL as a theory in typed λ-calculus
Henkin Models of HOL
Boolean and Functional Extensionality
Relationship of Categorical Semantics to Henkin Semantics (Time Permitting)
The following slides are from the first several lectures of the Winter 2006-2007 course.