Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage...
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 and SAT 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).
Lectures plan and links where connecting for following the lectures willbe communicated to the students who have registered in TISS.
Students have to prepare presentations of selected research articles on topics treated in this course.
Lecture 15hAdditional reading 30hOral exam, through a presentation (preparation+exam) 30h
(3 ECTS = 75 Hours)
Please register for this course if you want to participate.
Further information: http://www.star.dist.unige.it/~marco/SSTKR-2019/
Presentation and Oral Exam.
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.