COMPUTATIONAL LOGIC
- Overview
- Assessment methods
- Learning objectives
- Contents
- Bibliography
- Delivery method
- Teaching methods
- Contacts/Info
Knowledge of basic concepts of discrete mathematics is required. In the course the basic notions of propositional and predicate logic will be summarized, but some prior knowledge is advisable.
The exam consists of a written exam based on the resolution of the exercises related to the subjects discussed in the course and on theoretical questions, followed by an optional interview in which, besides supplementing and correcting the written test exercises, the focus will be on the assessment of the acquisition and of the correct understanding of the content of the course.
The course aims to provide basic knowledge of how logical systems can be used to deal with computational issues, in particular in relation with model checking, program verification and binary decision diagrams. Such knowledge is aimed at forming and increasing the abstraction of information through symbolic representation and thus the ability to understand an abstract and symbolic scientific language.
At the end of the course the student will be able to:
1. Know the basic logical systems, propositional and predicative logic, temporal logic and modal logic
2. Know and apply the basic SAT solvers
3. Know how to write programs in logic programming (Prolog)
4. Understand tools and properties of model checking
5. Know and apply the NuSMV model checker
6. Understand program verification and know Hoare triples
7. Know binary decision diagrams and their algorithms
Expected learning outcomes include the ability to identify any errors in computational argument, and to have the ability to use a formal language for the description of computational problems.
Propositional logic, truth tables, satisfiability and validity, SAT solvers (linear and cubic) (6h, objective 1)
Predicate logic, language, semantics and expressivity, clauses and resolution (6h, objective 2)
Logic programming, basic examples, recursion, lists and non-logical features (8h, objective 3)
Linear temporal logic, syntax and semantics. Branching time logic (6h, objective 4)
Model checking: Systems, tools and properties. The NuSMV model checker (8h, objective 5)
Program verification, Hoare triples, proof calculus (8h, objective 6)
Binary decision diagrams, algorithms for binary decision diagrams and symbolic model checking (6h, objective 7)
Course notes will be available on the web site.
Other suggested reading are:
• Mathematical Logic for Computer Science, by Mordechai Ben-Ari, Springer
• Logic in Computer Science: Modelling and Reasoning about systems, by Michael Huth and Mark Ryan, Cambridge University Press.
Lectures (48 h). The lessons aim at presenting multiple aspects of computational logic, as well as practical applications of the proposed topics.
The teacher receives by appointment, upon request by e-mail to brunella.gerla@uninsubria.it
Borrowed from
click on the activity card to see more information, such as the teacher and descriptive texts.