COMPUTATIONAL LOGIC
- Overview
- Assessment methods
- Learning objectives
- Contents
- Full programme
- 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 scope of the exam is to certify that students have all knowledge and ability explained above, by evaluating the knowledge skill and the ability to understand and then to expose the logical contents of the course.
The exam consists in an oral discussion during which the student has to talk on two topics chosen from a list proposed by the teacher. Final mark (out of 30) depends on the completeness and correctness of the exposition (70%), the clarity of the exposition (20%) and adequateness of answers (10%).
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)
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
Professors
Borrowers
-
Degree course in: COMPUTER SCIENCE