Einführung

The course provides an introduction to automated reasoning.

The course is open to master students, but in exceptional cases bachelor students can take part.

The following topics will be discussed:

• SAT/SMT
• automated theorem proving for first-order logic, resolution
• paramodulation, and orderings
• tableaux
• automated reasoning in higher-order logic

Zeitplan

The course will include several longer slots in order to end before the end of the semester.

VU

Donnerstag

11:15 – 13:30

3W04 (ICT-Gebäude, 2.Stock)

Lehrender

		Raum	Sprechstunde
VU	Cezary Kaliszyk	3M12	Mittwoch	11:15 – 12:45

Voraussetzungen

The students are expected to have completed the courses on functional programming, logic, and term rewriting before attending this course.

Benotung

The course will be evaluated by means of assignments, presentations, and a final test, all contributing equally to the final grade.