Dr. Wolfgang Bibel, Professor

• Deduction
  Deduction is a central mechanism on which many AI activities are based. The connection method provides the logical basis for automated theorem proving carried out in our group. Several theorem provers for first-order predicate logic have been developed. Thereby we aim at integrating as many special techniques as possible within the general framework of the connection method. Machine-oriented connection proofs are transformed into a form appropriate for human understanding.
• Knowledge Representation
  Knowledge is an essential part for achieving intelligent behavior. We are committed to a logical form of representing knowledge since this allows the import of great reasoning power from deduction. Over the time many aspects of reasoning have been studied by members of the group such as non-monotonicity, modalities, fuzziness and so forth.
• Program Synthesis
  The automation of software production by way of synthesis from declarative specifications is considered one of the most problems for Artificial Intelligence. In the recent years we have pursued the proofs-as-programs paradigm in constructive logics. This led to the development theorem provers for intuitionistic logic on the basis of those developed for classical logic so that all features from those could be imported. The work is pursued in the framework of the NuPRL verified program development system.
• Logic Programming
  Equational theories are of importance in many areas of computer science and AI. To incorporate such theories into a deductive mechanism like the one used in logic programming, enhanced unification algorithms are studied and extensions of the standard resolution strategies (which on Horn clauses are identical with connection method strategies) are explored.
• Reasoning about Actions
  To solve the classical AI planning problem several approaches based on the resource paradigm have been developed and are still being explored. In particular, we were able to solve the frame problem this way. On this basis we investigate ontological extensions such as non-deterministic and concurrent actions, the ramification problem, and hierarchical planning. Furthermore, we have explored, extended and compared high-level specification languages such as A (Gelfond and Lifschitz) and the Ego-World-Semantics (Sandewall).
  An assistance planning system has been designed and is used to develop and verify interactive planning methods to support a human user.
• Connectionistic Systems
  Connectionism bases on the idea of parallel distributed processing. On the model of the human brain, artificial neural networks break up complex tasks into numerous parallel subtasks. Our group has been interested especially to model reasoning in such systems in order to get some understanding how reasoning might be realized in the brain.
• Stochastic Search
  Stochastic Search methods can be used to solve hard combinatorial optimization problems efficiently. In this field we work with stochastic search methods for the solution of satisfiability problems (SAT) and Constraint Satisfaction Problems. We aim to develop massively parallel search methods, based on neural networks, for the solution of SAT. Search methods inherent in natural systems are studied for the solution of hard combinatorial optimization problems. Here our research focuses on ant colony optimization, an approach which models the behavior of ant colonies and is used to solve function or combinatorial optimization problems.

Current Projects:

Courses: