The goal of this lecture is to provide students with an understanding
how solving techniques are designed and implemented in state-of-the-art
systems. They become familiar with some of the most advanced methods
developed in the areas of AI and knowledge representation. This will
increase their ability to detect similarities among solving strategies
in different domains and thus the ability to migrate solving techniques
to other reasoning paradigms.

The course starts on Thu Oct 12 at 13:00 in Seminarraum von Neumann (Favoritenstraße 9-11) with a preliminary meeting (organization of this course).

The main part of the course starts on Oct 19 (which is also the deadline for the registration).

Declarative knowledge is expressed by means of declarative sentences
in a symbolic language, and such knowledge is processed by running a
reasoning procedure that works on these sentences. In order to deal
with problems of real-world size, software systems that implement such
kind of knowledge processing (often called provers or solvers) require
advanced methods that take advantage of mature technology.  Moreover,
for performance heuristics, space-efficient data-structures and
parallelization techniques become crucial. This lecture shall give an
overview on such state-of-the-art methods and techniques. It will
also introduce students to the respective systems and tools.

The course focuses on Answer-Set Programming and its
extensions (as a representative for related formalisms such as SAT
and Constraint-Satisfaction formalisms). It further captures
hybrid-formalisms (integration of ASP with other formalisms).

This lecture complements the related course about "Processing
of Declarative Knowledge" (184.700) which focuses on the modelling
aspect of declarative programming. This course, on the other hand,
shall provide deeper insight in the computational methods developed
for efficient evaluation of the modelled problem.  Compared to the
course "SAT Solving and Extensions" (184.090), the focus is here on
more powerful languages (e.g., supporting predicate language) which
therefore require techniques which go beyond the standard DPLL
procedure as employed in SAT-solvers (e.g., grounding, unification etc).

Lecture Units (all in Seminarraum von Neumann, Favoritenstraße 9-11):

• Oct 12, 2017, 13:00-14:00: Preliminary Meeting (Organization and Introduction)
• Oct 19, 2017, 13:00-16:00: Recapitulation and Solver Architecture
• Nov 9, 2017, 13:00-16:00: Grounding
• Nov 16, 2017, 13:00-16:00: Solving
• Nov 23, 2017, 13:00-16:00: ASP Extensions
• Nov 30, 2017, 13:00-16:00: Other Solving Techniques
• Jan 11, 2018, 13:00-18:00: Presentation of exercises and projects

ECTS breakdown:

Lecture 15h
Small project 30h
Optional exercises 8h
Presentation of project and exercises 5h
Oral exam (preparation+exam) 17h

(3 ECTS = 75 Hours)

Please register for this course if you want to participate.

The course consists of the following parts:

• Lectures which provide the necessary background.
• Project: The default topic is to implement selected reasoning algorithms (a "simple ASP solver") to improve your understanding of the techniques, where the programming language is of your choice. However, alternative (theoretical or practical) topics in the scope of this course depending on individual interests are possible. If you don't like to implement, don't hesitate to ask for an individual topic.
• Optional exercises announced during the lectures (bonus points).
• Presentation of the project and discussion of the optional exercises in a dedicated course unit.
• Final oral exam.

Registration is required if you want to participate.

Attendance in the lectures is not mandatory but encouraged. However, there will be a dedicated course unit towards the end of the semester where projects are presented and attendance will be required.

The course is for master and PhD students with background in formal logic.

Some experience in knowledge representation (in particular ASP) and algorithmics is helpful, but not strictly necessary for successful participation.

For the suggested default project (implementing reasoning algorithms), some programming experience in a programming language (of your choice) is required. However, the goal of the project is to get a better understanding of the presented reasoning techniques by implementing some of them, not the development of a full-fledged solver. Also, alternative project topics are possible. Hence, you don't have to be a professional software engineer to take the course!