Elmar Eder

[That's me]

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.

Visits as a visiting researcher at


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

Previous fields of work

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)





Snail mail

Elmar Eder
Department of Computer Sciences
University of Salzburg
Jakob-Haringer-Str. 2
5020 Salzburg
Persönliche Links
file last modified: Thursday, 19-Jan-2012 09:15:20 CET