Abschlussarbeit

Description:

The field of knowledge representation and reasoning has developed a multitude of important and deep theoretical insights on artificial intelligence. Many of these results are proven by hand. The community of automated reasoning has developed powerful tools for checking theorems mechanically. Typical theorem provers are Isabelle (https://isabelle.in.tum.de/), LEAN (https://lean-lang.org/), Leo (http://leoprover.org) or Coq (https://coq.inria.fr/).

A potential topic for a thesis is formalizing a well-known theorem within the language of a proof assistant. Our emphasis is on theorems in non-monotonic reasoning, theory change, or argumentation. If you are interested in such a topic for your thesis, please get in touch with Dr. Kai Sauerwald.