LOGIC FOR ARTIFICIAL INTELLIGENCE
- Overview
- Assessment methods
- Learning objectives
- Contents
- Full programme
- 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 artificial intelligence and knowledge representation. 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, binary decision diagrams and their algorithms
3. Know how to write programs in logic programming (Prolog) for representing knowledge
4. Know how to deal with pure declarative programming (Answer Set Programming) for planning problems and for finding solutions to puzzles and games
5. Understand tools and properties of model checking, know and apply the NuSMV model checker
6. Know how to deal with uncertainty and vagueness in reasoning, using probabilistic and fuzzy logic
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, predicate logic, language, semantics and expressivity, clauses and resolution (8h+ 2h exercises, objective 1)
Linear temporal logic, syntax and semantics. Branching time logic (4h +2h exercises, objective 1)
SAT solvers (linear and cubic), Binary decision diagrams, algorithms for binary decision diagrams (6h+4h exercises, objective 2)
Logic programming, basic examples, recursion, lists and non-logical features, Logic for knowledge representation, SWI-PROLOG (10h + 6h exercises, objective 3)
Answer set programming, pure declarative paradigms, logic programming for solving games and puzzles, CLINGO (10 h+6h exercises, objective 4)
Model checking: Systems, tools and properties. The NuSMV model checker (10h+4h exercises, objective 5)
Probabilistic and fuzzy logic to deal with uncertainty and vagueness in reasoning (8h, objective 6)
Propositional logic, truth tables, satisfiability and validity, predicate logic, language, semantics and expressivity, clauses and resolution (8h+ 2h exercises, objective 1)
Linear temporal logic, syntax and semantics. Branching time logic (4h +2h exercises, objective 1)
SAT solvers (linear and cubic), Binary decision diagrams, algorithms for binary decision diagrams (6h+4h exercises, objective 2)
Logic programming, basic examples, recursion, lists and non-logical features, Logic for knowledge representation, SWI-PROLOG (10h + 6h exercises, objective 3)
Answer set programming, pure declarative paradigms, logic programming for solving games and puzzles, CLINGO (10 h+6h exercises, objective 4)
Model checking: Systems, tools and properties. The NuSMV model checker (10h+4h exercises, objective 5)
Probabilistic and fuzzy logic to deal with uncertainty and vagueness in reasoning (8h, objective 6)
56h lectures + 24h Exercises. The lessons aim at presenting multiple aspects of mathematical logic in the realm of artificial intelligence, as well as practical applications of the proposed software.
The teacher receives by appointment, upon request by e-mail to brunella.gerla@uninsubria.it