28 February: fyi -- research, Saarbruecken
Index of February 2001 | Index of year: 2001 | Full index
Research interests and OMEGA project outline
Our research concentrates on the development of the mathematical
assistant system OMEGA. In contrast to traditional theorem proving
systems, OMEGA employs the proof planning paradigm and tries to
support the mathematician at a cognitively adequate conceptual
level. Instead of dispensing with the strengths of powerful
traditional reasoning systems however, we integrate them as support
systems. For this purpose an agent based framework is developed
supporting the distribution and cooperation of external reasoning
systems via the internet. The OMEGA core system is implemented in
multi-processing CLOS (object oriented Lisp) and various other
programming languages such as Oz and Java are used by outsourced
modules like the graphical user interface LOUI. The core logic of
OMEGA is a higher order logic based on Church's simply typed lambda
calculus.
The main lines of research include:
Proof Planning: Proof planning is a technique to abstract from proof search on pure calculus level by grouping
frequently recurring low level proof patterns into proof methods. Search is employed to construct a proof plan
composed of chains of proof methods. This planning process is guided at the meta level by proof strategies. Our
current work focuses on the development and improvement of our multi strategy proof planner.
Human Computer Interaction: OMEGA provides an agent-based suggestion mechanism supporting interactive
theorem proving and mixed-initiative proof planning. Communication with the user is realized via the graphical user
interface LOUI. One of our projects develops P.rex, which is an interactive, user adaptable proof verbalization and
proof explanation system. Another project on natural language processing, which aims at a spoken dialog with a
mathematical assistant system, is in preparation.
Agent Based Integration of External Reasoners: OMEGAs agent-based subsystem O-ANTS provides a flexible
mechanism to integrate various external reasoning systems. The mathematical software bus MathWeb supports their
distribution over the Internet. Future research will be to combine these mechanisms more closely with OMEGAs
proof planner and to employ the meta knowledge of the proof planner also to guide the agent based layer.
Proof Transformation & Representation: Our system integration approach is a skeptical one and we develop
modules for translating results of external reasoners into OMEGAs central proof object. We only trust these results
when they can be proof checked in OMEGAs core calculus. Current work includes the transformation of computer
algebra computations or higher order resolution style proofs.
Acquisition & Representation of Mathematical Knowledge: Proof planning is a knowledge intensive approach and
presupposes the acquisition and representation of very large databases of mathematical knowledge (e.g. theorems,
lemmata, definitions, methods, mathematical strategies, etc.). To store and maintain this knowledge the mathematical
database MBASE is developed as a universal repository of formalized mathematics. MBASE is currently under
development in Saarbrücken and at Carnegie Mellon University in Pittsburgh, USA.
Applications in Maths Learning: As an interesting application and in order to evaluate our system we integrate and
use it interactively in the ActiveMath system, which is a web-based learning environment for mathematics.
The OMEGA group currently consists of 11 full time researchers and about twice as many students.
Cooperations:
In Saarbrücken we are a part of the interdisciplinary Collective Research Centre (SFB378: `Resource adaptive
cognitive processes') and thereby cooperate with the Computational Linguistics Department. The maths learning
project is realized at the German Research Center for Artificial Intelligence (DFKI).
Internationally we are coordinating the CALCULEMUS Network funded under EU 5th framework which links IRST in
Trento (I), RISC in Linz (AUT), and the universities of Edinburgh (UK), Birmingham (UK), Genua (I), Eindhoven
(NL), Karlsruhe (D), and Bialystok (POL).
Further cooperation exists with Carnegie Mellon University in Pittsburgh (USA), CORNELL University in Ithaca
(USA), University of Budapest (HUN), and ITESM-Campus Ciudad de México (MEX).
We are also involved in several projects on teaching software under the new initiative of the German government.
The Candidate:
We are looking for highly motivated candidates willing to work in an internationally oriented team with a good background in
at least two of the following directions:
Artificial Intelligence; especially Planning, Agent based Reasoning, Knowledge Representation, Learning
Mathematical Logic and/or Mathematics
Interactive or Automated Theorem Proving
Human Computer Interaction and knowledge based natural language presentation
Databases and Web-Technology
Implementational skills (optimally in a functional and/or concurrent programming language) and experience in the
development of large systems
The candidate should have an M.Sc. or PhD (or equivalent degree) in Computer Science, Mathematics, or Computational
Linguistics and should be able to speak and write in English. German is optional but helpful for social reasons. The
opportunity to produce a PhD thesis in the context of one of our projects will be given.
The Salary:
The positions are available immediately. Payment will be according to BAT2a on the German scale for federal employees.
BAT2a amounts to an annual salary of approx. 68 000.- to 86 000.- DM before tax depending on age and family status.
Contact Addresses:
Please send your application (including a CV, a list of publications, and a list of realized projects) to
Dr. Christoph Benzmüller
Fachrichtung Informatik
Universität des Saarlandes
Postfach 151150
D-66041 Saarbrücken
Germany
(chris@ags.uni-sb.de)
Prof. Dr. Jörg Siekmann
Universität des Saarlandes / DFKI
Stuhlsatzenhausweg
D-66123 Saarbrücken
Germany
(siekmann@dfki.de)
Index of February 2001 | Index of year: 2001 | Full index