The goal of this lecture is to provide students with an understandinghow solving techniques are designed and implemented in state-of-the-artsystems. They become familiar with some of the most advanced methodsdeveloped in the areas of AI and knowledge representation. This willincrease their ability to detect similarities among solving strategiesin different domains and thus the ability to migrate solving techniquesto other reasoning paradigms.
The course starts on Thu Oct 6 at 13:00 in Seminarraum von Neumann (Favoritenstraße 9-11) with a preliminary meeting (organization of this course).
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 sentencesin a symbolic language, and such knowledge is processed by running areasoning procedure that works on these sentences. In order to dealwith problems of real-world size, software systems that implement suchkind of knowledge processing (often called provers or solvers) requireadvanced methods that take advantage of mature technology. Moreover,for performance heuristics, space-efficient data-structures andparallelization techniques become crucial. This lecture shall give anoverview on such state-of-the-art methods and techniques. It willalso introduce students to the respective systems and tools.
The course focuses on Answer-Set Programming and itsextensions (as a representative for related formalisms such as SATand Constraint-Satisfaction formalisms). It further captureshybrid-formalisms (integration of ASP with other formalisms).
This lecture complements the related course about "Processingof Declarative Knowledge" (184.700) which focuses on the modellingaspect of declarative programming. This course, on the other hand,shall provide deeper insight in the computational methods developedfor efficient evaluation of the modelled problem. Compared to thecourse "SAT Solving and Extensions" (184.090), the focus is here onmore powerful languages (e.g., supporting predicate language) whichtherefore require techniques which go beyond the standard DPLLprocedure as employed in SAT-solvers (e.g., grounding, unification etc).
Lecture Units (all in Seminarraum von Neumann, Favoritenstraße 9-11):
ECTS breakdown:Lecture 18hSmall project 30hOptional exercises 5hPresentation of project and exercises 5hOral 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:
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!
