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