| Course: | Theory of Computing |
|---|---|
| ID: | BZ- |
| Authors: | Diego Calvanese |
| ECTS: | 8 |
| Classification: | |
| Description: | The objective of the Theory of Computing course is to introduce and study abstract, mathematical models of computation (such as finite state machines, push down machines, and Turing machines), and to use the abstract machine models to study the ability to solve computational problems, by identifying both the intrinsic limitations of computing devices, and the practical limitations due to limited availability of resources (time and space). A second objective is to show how to reason and prove properties about computing in a precise, formal, abstract way. The syllabus includes: Regular languages (finite automata and regular expressions); Context-free languages (context-free grammars, pushdown automata); Turing Machines; Undecidability; Computational complexity; NP-completeness; Polynomial hierarchy. |
| Course: | Knowledge Representation |
|---|---|
| ID: | BZ- |
| Authors: | Enrico Franconi |
| ECTS: | 4 |
| Classification: | |
| Description: | The aim of the course is to provide students with an understanding of the formal foundations of classical logic-based knowledge representation languages, and with an overview of the reasoning methods for them. Most of the course will focus on description Logics and on ontology languages. Other formalisms will be introduced, such as modal logics, temporal logics and epistemic logics. The syllabus includes: A review of computational logic; Knowledge Representation; Structural description logics; Propositional description logics; Knowledge bases; Modal logics; Logics and databases. |
| Course: | Computational Logic |
|---|---|
| ID: | BZ- |
| Authors: | Pablo Fillottrani |
| ECTS: | 4 |
| Classification: | There are no prerequisites in terms of courses to attend. Students must be familiar with propositional and first order logic, and must have practical experience in logic programming. Objectives The objective of this course is to offer a comprehensive introduction of the methods and techniques in Computational Logic. Although the course has a formal background, it includes a strong practical part in using automated tools and with a review of applications. The syllabus includes: Computational Logic: motivation and importance of the field; Propositional and First Order Logic: deduction, proof theory, automated theorem proving; Higher Order Logic; Induction and Abduction; Non-monotonic reasoning; Applications of Computational Logic. |
| Description: |
| Course: | Non-classical Logics |
|---|---|
| ID: | BZ- |
| Authors: | Rosella Gennari |
| ECTS: | 4 |
| Classification: | |
| Description: | Modal logic is usually viewed as the logic of 'necessity' in philosophy, and of 'provability' in mathematics. But computer science has advocated another view: that of modal languages as compact yet expressive languages for describing relational structures. In fact relational structures - hence modal logic - lie at the core of computer science areas such as computational linguistics, planning and (concurrent) program verification. This course will present the basics of modal logic, emphasizing its semantic and computational properties. The syllabus includes: Basic concepts: relational structures, in particular transition systems and trees; modal languages; semantics of modal logics; proof systems for modal logics; Models and satisfiability:basic model construction techniques; simulations and bisimulations; the standard translation; Frames and validity; Soundness and completeness of the basic modal logic; Decidability of the basic modal logic. |
| Course: | Formal Methods |
|---|---|
| ID: | BZ- |
| Authors: | Alessandro Artale |
| ECTS: | 4 |
| Classification: | |
| Description: | In this module students will develop a deeper understanding of technologies based on applying formal methods for the specification and verification of hardware systems. Students will learn the most important techniques based on Model Checking to check properties of a system. In particular, the student will be able to understand how to formally specify an hardware system by means of transition systems and how to express computation properties by means of formulas in Temporal Logic. Both Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) will be studied together with efficient algorithms for model checking formulas in these logics. During the lab a tutorial on NuSMV will introduce the student to one of the most successfull software used in industrial applications to specify and test syncronous concurrent systems and critical software. |
| Course: | Programming Languages |
|---|---|
| ID: | BZ- |
| Authors: | Alessandro Cimatti |
| ECTS: | 4 |
| Classification: | |
| Description: | The aim of the course is twofold. On one side, we aim at building substantial hands-on programming skills with LISP and PROLOG. On the other side, we will provide basics notions in functional, logic and constraint programming. LISP: Symbols; basic functions; definitions, predicates, scoping; recursion, tail recursion, and iteration; lambdas; properties, a-lists, arrays; reading and printing; macros; memory management, destructive lisp; interpretation and compilation; foundations, elements of lambda caclulus. PROLOG: Facts, rules and queries; matching and proof search; recursion; terms; cuts and negation; database manipulation; collecting solutions; working with files. CONSTRAINT LOGIC PROGRAMMING: Semantics of logic programs; constraints; constraint handling rules; principles of constraint solving (variable elimination, local consistency); examples of common constraint systems (Boolean, linear polynomilal, finite domains, interval). |
| Course: | Mathematical logic |
|---|---|
| ID: | PSW |
| Authors: | Stefano Baratella |
| ECTS: | 6 |
| Classification: | 1.1.1 |
| Description: | Formative aims: Formal methods are increasingly used as powerful specification, verification and early debugging methods in the development of industrial SW and HW systems. This course provides an introduction to Formal Techniques and Tools for the specification and verification of Hardware and Software platforms. Apart from an introduction on formal techniques and their benefits, the course will concentrate mainly on formal verification and techniques and, in particular, on Model Checking (MC). A laboratory will be given in which the students will experience MC techniques by means of the MC NuSMV and SPIN. Program of the course: The course covers propositional logic, first order logic and basic modal logics. Topics in logic include syntax, semantics, models, logical entailment, proofs, soundness, completeness, and decidability. Reasoning methods include the truth table method, natural deduction, the Davis-Putnam procedure, resolution and tableaux methods. |
| Course: | Formal Methods |
|---|---|
| ID: | PSW |
| Authors: | Roberto Sebastiani |
| ECTS: | 12 |
| Classification: | 1.1.3 |
| Description: | Formative aims:
Making students capable to use the basic logic methodologies for
representing knowledge in a computer, and for performing automated
inference on it. To reach the goal, we will provide a rigorous
introduction to logic form a representational and computational
perspective.
Program of the course:
The main topics presented in the course are:
|
| Course: | Automated Reasoning for AI |
|---|---|
| ID: | VU-AR |
| Authors: | dr. K.S. Schlobach, dr. H.E. Wache, prof. dr. F.A.H. van Harmelen |
| ECTS: | 6 |
| Classification: | 1.1.1.2, 1.1.3 |
| Description: | The course will be structured in three modules. In
each of these modules a practical problem will be introduced, a
logic-based representation proposed, and the basic techniques for
automated reasoning in this language studied in a practical, hands
on, way.
In a nutshell, we plan to cover:
|
| Course: | Advanced Logics |
|---|---|
| ID: | VU-AL |
| Authors: | dr. R.C. de Vrijer |
| ECTS: | 4 |
| Classification: | 1.1.1.4, 1.1.3 |
| Description: | Modal logic are already shortly introduced in the course introduction logic. This course deepens the insight and skills in modal logic, with a view to applications in data processing and artificial intelligence. Modal logic exists in several variants, for example time logic, logic, dynamic logic, deontische logic. All these forms have their own specific applications. But the theoretical framework is always the same: Kripke-models with possible worlds. Important technical appliances for investigating modal logic are comparisons of Kripke models. |
| Course: | Intelligent Systems in the WWW (Advanced) (Intelligente Systeme im WWW II) |
|---|---|
| ID: | KA:IS2 |
| Authors: | Hitzler, Sure |
| ECTS: | 4.5 |
| Classification: | 1.1, 1.1.1, 1.1.2, 1.1.3 |
| Description: | Goal of this course will be to extend knowledge on logics and reasoning. The course will be held in German. |