Introduction

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

Schedule

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

VU

Thursday

11:15 – 13:30

3W04 (ICT building, 2nd floor)

Lecturer

		room	consultation hours
VU	Cezary Kaliszyk	3M12	Wednesday	11:15 – 12:45

Prerequisites

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

Grading

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