This week, you will learn about ontologies as knowledge representations. We introduce the various types and classifications of ontologies. For the automatic processing of ontologies, we need a formal knowledge representation based on logics. Thus, we will recapitulate the very fundamentals of Propositional Logic (PL) as well as First Order Logic (FOL). Please note that this is not an introduction into mathematical logic, because you should already have a basic knowledge about mathematical logic. For an in-depth coverage on PL and FOL, please refer to the course literature. Next, we continue with the Tableaux Algorithm, an algorithm that enables automated reasoning. Basically, it is an algorithm based on the principle of 'Proof by Refutation', i.e. you proof an assumption by showing that its negation is wrong.
You will learn that FOL is not the best choice for a knowledge representation, simply because it is too difficult to handle (if it comes to decidability or runtime complexity of proof algorithms). Therefore, we are considering fractions of FOL, so-called Description Logics (DL), a family of languages for knowledge representation. You will learn to define ontologies with ALC, one of the most simple DLs, The lecture concludes with the adaption of the previously mentioned Tableaux Algorithm for the description logic ALC.
This lecture probably is the most 'theoretic' and 'formal' lecture of the entire course. In the next lecture, you will learn OWL, the Web Ontology Language, which is based on Description Logics, and we will construct ontologies with the help of OWL.