| Week |
Topic |
Wednesday (10:15:-11:45) |
Thursday
(15:45-19:00) |
| 1:Oct 07-13 |
FOL and CQs |
Lectures 1-2
- Introduction to the course
-
First-order logic
|
Lectures 3-6
- Open and closed formulas
- Logical implication
- Evaluation of a formula
|
| 2:Oct 14-20 |
FOL and CQs |
Lectures
7-8
- Time cost of evaluation
- Space cost of evaluation
- Combined complexity, Data complexity, Query complexity
| Lectures 9-12
- Theory of conjunctive queries (CQs)
- NP completeness of CQs evaluation
- Homomorphism
- Chandra-Merlin Theorem
|
| 3:Oct 21-27 |
Formalizing UML Class Diagrams |
Lectures 13-14
- UML class diagrams
- Fomalization in FOL
|
Lectures 15-18
- Fomalization in FOL
- Automated reasoning on UML class diagrams
- Complexity of reasoning on UML class diagrams
|
| 4:Oct 28-Nov 3 |
Formalizing UML Class Diagrams |
Lectures 19-20
- Incomplete databases
- Certain answers
- CQs in incomplete databases
|
Lectures 21-24
- CQs over UML class diagrams
- Complete vs incomplete information
- CQs over DLs KBs
- DL-liteA
|
| 5:Nov 4-Nov 10 |
Query Answering through UML Class Diagrams |
Lectures 25-26
- DL-liteA
- Query answering in DL-liteA
|
Lectures 27-30
- Reasoning in DL-liteA
- Semantics of programs
- Structural operational semantics
- Evaluation semantics
|
| 6:Nov 11-17 |
Semantics of programs |
Lectures 31-32
- Structural operational semantics
- Transition semantics
- Concurrency
|
Lectures 33-36
-
Hoare Logic |
| 7:Nov 18-24 |
Fixpoint theory |
Lectures 33-34
- Fixpoints
- Least and greatest fixpoints
- Knaster-Tarski theorem
- Approximates of least-fixpoint
- Approximates of greatest-fixpoint
- Approximates theorem |
Lectures 35-38
- Least and greatest fixpoints
- Approximates of least-fixpoint
and greatest-fixpoint
- Transition Systems
- Mu-calculus
|
| 8:Nov 25-Dec 01 |
Model checking |
Lectures 39-40
- Mu-calculus
- Propeties of mu-calculus
- Evaluating mu-calculus formulas over transition systems: model checking |
Lectures 41-44
- Introduction to model checking
- Transition systems
-
Temporal logics: LTL, CTL e CTL*
|
| 9:Dec 02-08 |
Model checking |
Cancelled
|
Cancelled
|
| 10:Dec 09-16 |
Model checking |
Lectures 45-46
- Linear time framework
- Linear time logic (LTL)
- Properties of LTL
- Expressing safeness, liveness and fainess properties in LTL
|
Lectures 47-50
- Brancing time framework
-
Computational Tree Logic (CTL)
-
Properties of CTL
- Expressing safeness, liveness and fairness properties in CTL
- Translation of CTL formulas into mu-calculus
-
Model checking in CTL via mu-calclulus modelchecking
- LTL, CTL are uncomparable from the point of view of expressiveness
-CTL*
|
| 11:Dec 17-22 |
Question time and exam exercises |
Lectures 51-52
- Model checking in the linear time framework
- Transition systems runs as infinite strings
- Buchi Automata on infinite strings
- LTL model checking as nonemptiness of Buchi automata
|
Lectures 53-56
-
Exam exercises
|
-->