Automated Reasoning

The study of automated reasoning helps produce programs that allow computers to solve reasoning tasks. In our group, this particularly regards the development and study of systems which compute solutions for logic programs or answer queries over a knowledge base like ontologies based on description logics.

Proof Systems

For most logic-based formalisms, it is possible to provide a system of rules which accurately describes the underlying reasoning process of said formalism. Generally, this regards justifying why a particular answer following from a query and a knowledge base or why something is entailed by a theory. This gives a precise characterisation of the steps needed to derive something from the formalism. This derivation, i.e. the needed steps, is called a proof. The system providing those proofs can then be studied for its theoretical properties or be implemented, providing an automated method for query answering or reasoning.

Complexity Analysis

The computational problems, arising from the research in our group or from the literature, generally need to be studied in terms of their worst case time and space complexity. Determining those properties is the topic of complexity analysis and its results enable us to give answers as to how fast and how efficient those problems can be solved independent of the particular algorithm.

• Knowledge Representation and Reasoning
  Modelling and processing information
• Knowledge-Enriched Data Management
  Reliable answers from unreliable data
• Neuro-Symbolic Reasoning
  Thinking Fast, Thinking Slow
• Declarative Problem Solving
  Solving problems by describing them

• back