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 6 at 13:00 in Seminarraum von Neumann (Favoritenstraße 9-11).

After that, there will be a guest talk on Oct 13. The main part of the course starts on Oct 27 (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 6, 2016, 13:00-14:00: Preliminary Meeting (Organization and Introduction)
• Oct 13, 2016, 13:00-16:00: Guest Talk by Marco Maratea
• Oct 27, 2016, 13:00-16:00: Recapitulation and Solver Architecture
• Nov 3, 2016, 13:00-16:00: Grounding
• Nov 10, 2016, 13:00-16:00: Solving
• Nov 17, 2016, 13:00-16:00: ASP Extensions
• Nov 24, 2016, 13:00-16:00: Other Solving Techniques
• Jan 12, 2017, 13:00-18:00: Presentation of exercises and projects

ECTS breakdown:

Lecture 18h
Small project 30h
Optional exercises 5h
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: Implementation of selected reasoning algorithms (a "simple ASP solver") to improve your understanding of the techniques. The programming language is of your choice.
• 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 with knowledge representation (in particular ASP) and algorithmics will be helpful, but is not a necessary precondition for successful participation.

For the project part, 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. Hence, you don't have to be a professional software engineer to take the course!