Elmar Eder

MACIS 2006 Paper

macis_Eder.tex and macis_Eder.ps

About me

I am a professor of Computer Science working in Automated Theorem Proving and Artificial Intelligence at the University of Salzburg. Here is my curriculum vitae.

• 1956 born in Wien (Vienna)
• At preschool age: first interest in mathematics and natural sciences, taught by my father; 1963 first occupation with differential and integral calculus and with Fourier series.
• At primary and secondary school exempted from mathematics courses; instead study of higher mathematics (at home taught by my father, at school autodidactic)
• 1968 student at the Ludwig-Maximilians-Universität München (Munich) in mathematics, physics, and mathematical logic while still attending secondary school.
• 1970 Vordiplom in mathematics at the Ludwig-Maximilians-Universität München
• 1971 graduation from secondary school in England.
• 1974 Diplom (Master's degree) in mathematics at the Ludwig-Maximilians-Universität München
• 1977 Doktorat (Ph.D.) in mathematics at the Ludwig-Maximilians-Universität München
• 1977-1982 researcher in General Relativity at the Max-Planck-Institut für Astrophysik in München
• 1977-1979 study of Computer Science at the Technische Universität München
• 1982-1986 researcher in my present field of work Automated Theorem Proving and Artificial Intelligence at the Technische Universität München
• 1986-1991 Gastprofessor (visiting professor) of Computer Science at the Universities of Dortmund, Hildesheim, Darmstadt, Duisburg, and Marburg in Germany
• 1990 Habilitation degree (needed in Germany as a qualification for a position as an associate or full professor) in Computer Science at the Universität Dortmund
• 1991-1992 C2-Hochschuldozent (associate professor) of Artificial Intelligence at the Universität Bonn in Germany
• Since 1992 professor of Computer Science at the Universität Salzburg in Austria: first Universitätsdozent (associate professor), then A.o.Univ.-Prof.

• Laboratoire d'Informatique Fondamentale et de l'Intelligence Artificielle in Grenoble, France
• Duke University in Durham, North Carolina, U.S.A.
• University of British Columbia (UBC) in Vancouver, Canada
• Institute for New Generation Computer Technology (ICOT) in Tokyo, Japan

Publications

Click here for a list of papers from where links to abstracts and to the papers (as gzip'd PostScript files) are under construction.

Research Interests

Present fields of work

• Artificial Intelligence
• Automated Theorem Proving
• Proof Calculi and their Complexities
• Logic Programming
• Theoretical Computer Science
• Complexity Theory

Previous fields of work

• Proof Theory
• Constructive Theory of Ordinals
• Recursion Theory
• General Theory of Relativity
• Scattering Problems in Electrodynamics
• Retarded Differential Equations
• Partial Differential Equations

Current research

My main field of research is the investigation of proof calculi for first order predicate logic with the goal of determining which calculi are suited for automated deduction. For an introduction to the subject see Chapter 3: Methods and Calculi for Deduction in the Handbook of Logic in Artificial Intelligence and Logic Programming, volume 1.

Subjects of my current research are the comparative study of calculi with respect to the lengths of shortest proofs of formulas as well as with respect to mutual simulatability, the efficient structure-preserving transformation to normal form (called definitional form) first introduced in the paper An Implementation of a Theorem Prover Based on the Connection Method, and the developement of new calculi and proof techniques such as the consolution calculus introduced in the paper Consolution and its Relation with Resolution. Most of my results in this area of research can be found in my book Relative Complexities of First Order Calculi.

The question whether backtracking is necessary in the connection graph resolution calculus is addressed in the paper Decomposition of Tautologies into Regular Formulas and Strong Completeness of Connection-Graph Resolution. An important issue in Automated Theorem Proving is a possible infinite branching of the search tree. One type of infinite branching is overcome by unification which can be applied more efficiently by using the lattice properties of the set of unifiers, established in the paper Properties of substitutions and unifications. This does not, however, solve the problem of infinite branching of the search tree for backward reasoning in proof calculi with a cut rule. First results on how to overcome these problems are presented in the paper Backward Reasoning in Systems with Cut.

For more information click here: current research.

Courses / Lehre (in German)

Addresses

Email

Snail mail

Elmar Eder
Department of Computer Sciences
University of Salzburg
Jakob-Haringer-Str. 2
5020 Salzburg
AUSTRIA, EUROPE