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.
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 knowledge
representation formalisms that are within the scope of this
course include Answer-Set Programming (and its extensions),
Description Logics, Constraint-Satisfaction formalisms, as well as
hybrid systems which aim at combining two or more knowledge
representation 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).
The course will be based on two main parts. The first part will consist of
lectures which provide the necessary background. In the second part of the
course the students prepare either a presentation of some paper(s) relevant
to the topic of the course, or carry out a project where they have to work
with systems discussed in the lecture.
The course is for master and PhD students with background in formal logic.
Some experience with knowledge representation and/or artificial intelligence
will be helpful, but is not a necessary precondition for successful
participation.
