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, such as propositional logic, first-order logic of fragments their of. The following are the main topics of this course:

  • Properties of the logics (finite model property, compactness property, tree model property, ...)
  • Basic reasoning tasks for knowledge representation (Satisfiability, Classification, Entailment Checking, ...)
  • Procedures for automated Reasoning (Tableau, Hypertableau, Resolution, Consequence-Based Reasoning, Automata Procedures)
  • Proving formal properties of the procedures (Soundness, Completeness, Termination)
  • Complexity of Algorithms



Wednesday: 16:00 — 17:30 in O27/3211
Thursday: 16:00 — 17:30 in O27/3211
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