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 and SAT 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).
Registration is required.
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.
