CloseHelpPrint
Kies de Nederlandse taal
Course module: NWI-IMC009
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
Academic year2017
Period
KW1-KW2  (04/09/2017 to 04/02/2018)
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
This course is not given in Nijmegen but in Eindhoven. In order to do it completely in Nijmegen, video recordings from the Eindhoven course will be made available, and meetings with the students will be arranged, typically one hour per two weeks.
For more information, contact the lecturer: Prof.dr. Hans Zantema or see http://www.win.tue.nl/~hzantema/arn.html
Teaching formats

• 32 hours lecture
• 136 hours individual study period
Additional comments
This course will not be taught as a regular course, but is available on video.
Topics
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, linear programming.

• Binary Decision Diagrams as efficient representation of boolean expressions.

• Unification; resolution on predicates.

• Reasoning modulo equations, term rewriting.
Test information
Written examination plus practical assignment, see website.In Eindhoven this course is 5ects. For upgrading it to the Nijmegen standard of 6 ects, some extra task should be executed.
Recommended materials
Handouts
available via http://www.win.tue.nl/~hzantema/ar.html
Instructional modes
Course occurrence

Lecture

Zelfstudie

Tests
Tentamen
Test weight1
OpportunitiesBlock KW2, Block KW3

CloseHelpPrint
Kies de Nederlandse taal