Exams and Grade
Introduction to Computational Logic
Core Course (Theoretical Computer Science), 9 credit points
Stammvorlesung (Theoretische Informatik), 9 Leistungspunkte
Summer Semester 2007
Prof. Gert Smolka,
Department of Computer Science,
Lectures are on Mondays, 11:15–13:00, and Wednesdays,
11:15–13:00, in Building E1.3, HS 002. The first lecture is
on Monday, April 16, and the last lecture is on Wednesday, July
18. The first tutorial is on Tuesday, April 24, and the last
tutorial is on Tuesday July 17. There will be no tutorials on
Tuesday, May 1 (Labor Day), and no lecture on Monday, May 28 (Pentecost).
Computational Logic plays an important role in many
areas of computer science, including verification of
hardware and software, programming languages,
databases and Artificial Intelligence. This course
lays the foundations for the more advanced core
courses Automated Reasoning, Semantics and
Verification. The main topics of the course are:
Last Change: Thu 01 Jan 1970 00:00:00 UTC
- Simply typed lambda calculus:
Syntax, semantics, deduction.
- Propositional logic:
completeness and canonicity, BDDs, resolution,
sequent calculus, natural deduction and Curry
- Higher order logic:
Higher order Boolean logic, quantifiers,
identity, extensionality, axiom of choice.
- Dynamic logic and computability: Regular
programs, weakest preconditions, invariants,
verification conditions, halting problem, theorems
of Rice and Gödel.