NWI-IMC009
Automated Reasoning
Course infoSchedule
Course moduleNWI-IMC009
Credits (ECTS)6
CategoryMA (Master)
Language of instructionEnglish
Offered byRadboud University; Faculty of Science; Informatica en Informatiekunde;
Lecturer(s)
Coordinator
prof. dr. H. Zantema
Other course modules lecturer
Lecturer
prof. dr. H. Zantema
Other course modules lecturer
Contactperson for the course
prof. dr. H. Zantema
Other course modules lecturer
Examiner
prof. dr. H. Zantema
Other course modules lecturer
Academic year2021
Period
KW1-KW2  (06/09/2021 to 30/01/2022)
Starting block
KW1
Course mode
full-time
Remarks-
Registration using OSIRISYes
Course open to students from other facultiesYes
Pre-registrationNo
Waiting listNo
Placement procedure-
Aims
Obtaining insight how various problems can be transformed to formulas, and can be solved automatically by computer programs manipulating these formulas.
Content
Many problems, in particular in the area of verification of computer systems, can be expressed as proving that some big formula is always true. In this course we will concentrate on various methods for treating this kind of problems. Not only correctness and completeness of these methods will be considered, also efficiency and usability. In particular we will consider:
  • Satisfiability of propositions: resolution and the main ingredients of modern satisfiability provers.
  • Satisfiability modulo theories, in particular using linear inequalities, and the underlying simplex algorithm.
  • Binary Decision Diagrams as efficient representation of boolean expressions, as the basis of symbolic model checking.
  • Unification; resolution on predicates.
  • Reasoning modulo equations, term rewriting.
Level
Master course.
Presumed foreknowledge
Basic knowledge of logic.
Basic programming skills.
Test information
Written examination plus practical assignment, see website.
Both parts should be at least 5; for the final grade they both count for 50 %.
Specifics
 
Recommended materials
Handouts
available via http://www.win.tue.nl/~hzantema/arn.html

Instructional modes
Course occurrence

Tests
Exam
Test weight1
Test typeExam
OpportunitiesBlock KW2, Block KW3

Assignment
Test weight1
Test typeAssignment
OpportunitiesBlock KW2