MACIS 2006 Paper
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
- 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
Click here for a list of papers from where links to abstracts and to the papers (as gzip'd PostScript files) are under construction.
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
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)
Department of Computer Sciences
University of Salzburg
file last modified: Thursday, 19-Jan-2012 09:15:20 CET