Newsflash
Recently I have moved to Innsbruck. Hence the data below is
slightly outdated. Please visit my homepage
in Innsbruck.
Introduction
I obtained my education at the
University of Technology,
Vienna.
In October 1996 I completed the master degree
"Computational Logic"
with submission of my
thesis
"Paramodulation Decision Procedures".
Computational Logic is a combined degree.
Teaching
in mathematics and computer science is provided.
In Novemeber 1996 I started my Ph.-D. program in Computer Science
with Mattias Baaz. This marks a shift of interest from automated theorem proving
to proof theory.
From Spring 1999 till Spring 2000 I worked on a
MSc (by resarch)
at the
Department of Pure Mathematics,
University of Leeds.
Participation in the research projects
- "Automated Model Building with Equality", P11624-MAT,
November 1996---May 1997.
- "Cut Elimination and Cut Introduction", P11934-MAT,
May 1997---January 1999
- Tools for the automated analysis of proofs; P14126-MAT.
May 2000---(till now)
For a more detailed description see my
vita, my list
of publications on
anonymous ftp, or visit one of my favorite webcities
Boneville or
PaulPope.
The easiest way to find me is to visit either a
book, a
comics or a
coffee shop.
Research Interest
- The mysteries of Hilbert's
Epsilon Calculus.
Instead of quantifiers the Epsilon Calculus makes use of a non-effective
choice function expressing (in the frame of number theory)
for a given statement A, the
"the smallest x satisfying A".
- Automatisation of (mathematical, proof-theoretic) reasoning.
There are many tools in symbolic computation supporting scientist and
technician but only few deal with the automatised analysis of
given proofs or documented decisions.
Software Projects
(or applications of automated theorem proving)
- The Incredible Logic Tool.
Together with Albert Brandl, Mandanda Eibegger, and Hans Hirschberger.
TILT automatically constructs a model, given a satisfiable set of
clauses. Given a unsatisfiable set of clauses it allows full control
over the underlying (refutational) theorem provers Otter &
SPASS;
kindly see
the 'offical' TILT page.
- CRes, Cut Elimination by Resolution.
CRes implements Cut Elimination by Resolution, a clever method
to assigning to each cut-formula in a given LK proof a set of
(unsatisfiable) clauses. The resolution proof serves as backbone
of the (almost) cut-free proof:
go forth and eliminate them
eliminate them.
As underlying theorem prover I use
SPASS.
Both project are application of resolution theorem provers. In
particular
CRes aims at providing proof theory with computational tools
which should simplify the actual calculation with proofs.
Kurt Gödel Society
The
Kurt Gödel Society
is an international organisation for the promotion of
research in the areas of Logic, Philosophy,History of Mathematics,
above all in connection with the biography of Kurt Gödel, and in other areas
to which Gödel made contributions, especially mathematics, physics, theology, and
philosophy. Currently I am Deputy Secretary of the KGS.
See the homepage for further information
how to apply for membership, benefits of membership and general outline
of activity of the society.
>go to Open Page and type the
>html-address of the page you want.