SluitenHelpPrint
Switch to English
Cursus: NWI-IMC009
NWI-IMC009
Automated Reasoning
Cursus informatieRooster
CursusNWI-IMC009
Studiepunten (ECTS)6
CategorieMA (Master)
VoertaalEngels
Aangeboden doorRadboud Universiteit; Faculteit der Natuurwetenschappen, Wiskunde en Informatica; Informatica en Informatiekunde;
Docenten
Docent
prof. dr. H. Zantema
Overige cursussen docent
Contactpersoon van de cursus
prof. dr. H. Zantema
Overige cursussen docent
Collegejaar2016
Periode
KW1-KW2  (29-08-2016 t/m 29-01-2017)
Aanvangsblok
KW1
Onderwijsvorm
voltijd
Opmerking-
Inschrijven via OSIRISJa
Inschrijven voor bijvakkersJa
VoorinschrijvingNee
WachtlijstNee
Plaatsingsprocedure-
Cursusdoelen
Obtaining insight how various problems can be transformed to formulas, and can be solved automatically by computer programs manipulating these formulas.

Inhoud
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
Bijzonderheden
This course will not be taught as a regular course, but is available on video.
Onderwerpen
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.
Toetsinformatie
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.
Werkvormen

• 32 hours lecture
• 136 hours individual study period
Werkvormen
Cursusgebeurtenis

Hoorcollege

Zelfstudie

Toetsen
Tentamen
Weging1
GelegenhedenBlok KW2, Blok KW3

SluitenHelpPrint
Switch to English