PROPOSITIONAL AND PREDICATE LOGIC. Syntax, semantics, and calculus (sequent calculus). RESOLUTION AND LOGIC PROGRAMMING. Unification algorithm and resolution. BINARY DECISION DIAGRAMS. Representation of Boolean functions using OBDDs. Boolean operations with OBDDs. PROGRAM VERIFICATION. Hoare triples. Verification rules. MODAL LOGIC. Syntax, semantics of modal logics. LOGIC FOR SECURITY. BAN logic.
Prerequisites for admission
- Andrea Asperti, Agata Ciabattoni, Logica a Informatica McGraw-Hill, 1997. - Michael Huth , Mark Ryan. Logic in Computer Science: modelling and reasoning about systems (2nd edition), Cambridge University Press, 2004. - Slides and other materials available on the course website.
The exam is a written test. The written test requires the solution of application and theoretical exercises, having contents and difficulties similar to those shown in class. During the exam, the consultation of texts or notes is not allowed. The evaluation parameters include: knowledge of the course topics and logical reasoning skills. In oder to pass the exam the score must be equal or above 18/30. The maximum score is 30/30 with laude. The marks will be sent to students by official e-mails, from the verbalization system.