Lecture: Algorithms for Knowledge Representation


This lecture course deals with the topic of formal Knowledge Representation and Reasoning. In this course we study algorithms that can process formalized knowledge and produce new implied consequences of this knowledge using so-called automated reasoning procedures. To formalize knowledge, we employ various logic-based formalisms from propositional logic and first-order logic to specialised Description Logics for knowledge representation. The following are the main topics of this course:

  • Properties of the logics (models, entailment)
  • Basic reasoning tasks for knowledge representation (satisfiability, classification, entailment checking, ...)
  • Procedures for automated Reasoning (tableau, resolution, consequence-based procedures)
  • Proving formal properties of the procedures (soundness, completeness, termination)
  • Complexity of algorithms



Tuesday: 16:00 — 17:30 in O28-H21
Wednesday: 10:00 — 11:30 in O27-H20
Consultations after the lectures or by appointment. If necessary, lectures can start 15 min later


Written examination. 


Tutorials take place during the lecture times, usually once in two weeks. The times for seminars and instructions for submitting exercises will be announced during lectures and in the Moodle e-Lerning System.

Lecture materials

All relevant lecture materials will be provided in Moodle. The password will be given at the lectures or can be requested per email from the lecturer. Lecture notes can be printed using the script printing service of SGI.

Supplementary Literature

Additional literature for the course (does not cover all topics):

  • Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi, Peter F. Patel-Schneider. The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press. 2007. 2nd edition. ISBN 978-0521876254
  • Uwe Schöning. Logik für Informatiker. 5th edition, Spektrum Akademischer Verlag, 2000 (ISBN 978-3827410054)
  • Melvin Fitting. First-Order Logic and Automated Theorem Proving. Springer. ISBN 0-387-94593-8
  • John Kelly. The Essence of Logic. Prentice Hall. ISBN 0-13-396375-6
  • John Sowa. Knowledge Representation. Brooks/Cole 1999

About this Course:

Type:Course for Master Studies (3L / 1E)
Credit points:6
Category:Theoretische und Mathematische Methoden der Informatik (Kernfach/Kernmodul)
Theoretische Informatik (Vertiefungsfach/Vertiefungsmodul)
Intelligente Systeme (Vertiefungsfach/Vertiefungsmodul)
Related courses:     Intelligente Handlungsplanung
Grundlagen des Semantic Web