Modules of EMCL

In this module students will develop a deeper understanding of some of the logics beyond first order logic. Students will be introduced to different of Modal Logics and they will be able to apply them to different area of Computer Science. In particular, they will appreciate the use of logics for the specification and verification of hardware systems, and they will learn how to use Model Checking to verify properties of systems.

After completion of the module students shall have fundamental knowledge of propositional and first-order logic and shall master the basic skills of these subjects. Moreover, they shall know the field of Computational Logic and its main subfields as well as the basic techniques and methods applied there.

The students shall get into contact with real applications of logic-based systems and get a feeling for how to apply the theoretical knowledge obtained in the other modules.

• Foundations of logic programming: unification, procedural semantics, declarative semantics, soundness and completeness of SLD-resolution, negation in logic programs, termination of logic programs;
• Foundations of constraint programming: complete constraint solvers, local consistency notions, incomplete constraint solvers, constraint propagation, search;
• Practice of logic programming: the programming language Prolog, recursion, special data structures and libraries, applications of logic programs.

The module addresses various types of domains for the variables of these problems, namely finite and continuous domains, and analyses their specificities as well as commonalities. The worst case and typical complexity of the underlying propagation algorithms is studied, together with their integration with both complete backtrack search and local search algorithms. In addition, some extensions of the pure constraint satisfaction paradigm are studied, namely optimization, soft constraints and universally quantified problems.

More specifically, the logical foundations address the analysis of the expressive power of query languages by relating them to appropriate fragments of some logic. Basic concepts and results of finite model theory are introduced to prove negative results on the expressive power (i.e., queries that cannot be expressed in a given query language). On the algorithmic side, methods for efficient query processing are presented and the complexity of several query languages is analyzed. This also comprises methods of multi-user synchronization in a single database systems or in a distributed environment and the trade-off between throughput of query processing and integrity. Advanced topics of this module address several aspects of data on the web. This includes methods for data extraction on the web (like wrapper generation and web data mining) as well as methods of information integration (like schema mappings, transformation of data, and data cleaning).

The main objective is that upon completion of this module, students have a detailed understanding of fundamental tasks and methods of data management. Students will thus have acquired the knowledge and skills needed to further develop and to make effective use of tools and systems for data management. This includes basic skills like taking the impact on query evaluation and optimization into account when formulating database queries in different ways. It also includes more advanced skills like the development of wrappers for web data extraction and solving problems in the context of integrating heterogeneous data sources.

The objective is that upon completion of this module, students will have acquired a solid understanding of computer-based systems and technology in a particular area, such that they are familiar with problems and solution approaches in it. Furthermore, it is expected that they are able to sets links to the knowledge and skills acquired on computational logic methods and techniques for possible deployment and application.

More specifically, the foundational side addresses predicate logic for knowledge representation, logic for databases, knowledge base design, and specific issues like update and change of knowledge. Important representation formalisms for the agenda are logic programs with negation, ontology languages, action languages, and logic-based agents, which are considered with their mathematical properties. Regarding inference, methods like deduction, common-sense reasoning (abduction, hypothetical reasoning etc), or non-monotonic reasoning in general are addressed. On the practical side, tools and methods for problem solving such as Answer Set Programming or SAT/Quantified Boolean Formula solving are covered. Areas like Multi-Agent Systems, Information Systems or the Web serve to embed the theoretical concepts into applications.

The main objective is that upon completion of this module, students have a detailed understanding of how knowledge is formalized and processed in Artificial Intelligence using logic-related approaches, and of problems and issues that have to be respected. They furthermore will have acquired skills in designing, formally specifying, and realizing techniques of knowledge representation and reasoning.

After completion of this module, the students have fundamental knowledge about results and techniques in selected topics, and master the subject at a level such that they are able to understand and follow research issues in the area, and that they are able to formulate and investigate research tasks appropriate for a master thesis.

The purpose of the course is to give an introduction to those techniques. This module is composed by two courses, one focusing on Languages and Models for Concurrency and Security, and other on Logics for Specification and Verification. The first course focuses presents some fundamental models of concurrent and secure systems, based on process algebras, and associated analysis techniques. The second course focuses on the use of logic as a language for both specification and verification, with some emphasis on temporal logics. Both modules will cover the use of by tools to support the analysis of specifications and the of verification of concrete systems.

The students learn the theoretical foundations of formal verification (model checking, interactive theorem proving) and get a deep understanding of the design, implementation and application of verification tools.

The main objective is that upon completion of this module, students have a detailed understanding of how knowledge is formalized and processed in ontology research using description logics, and of problems and issues that have to be respected. They furthermore will have acquired skills in designing, formally specifying, and realizing techniques of conceptual design, database access and integration.

To this end the module covers in its core theory of computability including models of computation, computable functions, recursion theory, limits of solvability, as well as computational complexity theory, including complexity measures, complexity classes, problem reduction and completeness. Topical aspects (e.g., emerging models of computation, applications in computational logic, or advanced algorithmic techniques) allow to gain additional knowledge and skills.

The main objective is that after completing this module, the students have a deep understanding of the theoretical foundations and the limits of computation. They also have a solid knowledge of complexity theory, which they can apply to establish complexity bounds and characterizations of computational problems in applications, and to develop algorithms for the solution of such problems. A further objective is that the students are able to reason and prove properties about computations in a precise, formal, abstract way.

After the completion of the module students will have a deeper understanding of the use of advanced formalisms which underpin the development and use of databases. In particular, they'll learn how to additional conceptual modelling methodologies beside the standard UML and ER design. In addition they will be able to leverage advanced data models which go beyond the standard relational model.

After completion of the module students have an in depth understanding of the development, implementation and application of inference techniques.

After the completion of this course, students will be familiar with technologies and formalisms which underpins the Semantic Web. Moreover, they will able to apply them in order to build semantically rich applications. In addition, students will have the possibility to complement their knowledge of Semantic Web by studying semantic based approaches to closely related research areas (e.g. Computational Linguistics).

After completion of the module the students have a deep and practically applicable knowledge of the methods from Theoretical Computer Science that are relevant for application in logic, as well as a good understanding of formal properties of various logics.

After completion of the module students are able to analyze a simple scientific problem, to relate the problem to the state of the art in the underlying sub-field, to solve the problem, to present the problem, the state of the art as well as the solution in written form as well as in an oral presentation, and to defend their claims.

After completion of the module students are able to present and to discuss scientific achievements.

The language course shall teach basics of the language of the country of the host university and the students shall acquire enough skills for coping with simple everyday challenges of communication in the language of their host country.