🚀 go-pugleaf

From: Bertram Fronhoefer <bertram@lan.informatik.tu-muenchen.dbp.de>
To: mod-ki@unido.informatik.uni-dortmund.de
Date: 12 Apr 90 16:23:44+0200
Subject: Zwei Summerjobs in Muenchen
Keywords: Stellen

mod-ki message 0431
************************************************************************
           S U M M E R  J O B
 
           Enhancing a Theorem Prover with Abstractions
 
Location:  Technical University Muenchen, West Germany
           AI research group
           Augustenstr. 46 RGB/II
           D-8000 MUENCHEN 2
 
Job Description:

Would you like to join us and help to extend our theorem prover ?

THE OVERALL PROJECT:
Durig the last years, we have  developped  a  powerful  theorem  prover,
called SETHEO. It is based  on  the  model  elimination  calculus.  High
efficiency is gained by compilation a` la Warren  Abstract  Machine.  It
compares  well  with  other  international  research  projects.  Current
research  interests  include  automated  learning  of  heuristics  by  a
connectionistic approach.

SPECIFIC PROBLEM FIELD:
In order to improve our theorem  prover,  in  particular  the  power  of
finding proofs, we are interested to incorporate the ideas published for
instance by D. Plaisted  "Theorem Proving with Abstraction"  (Artificial
Intelligence 16 (1981)). The idea is to simplify a formula to be  proved
by abstracting from some of its features (e.g. cutting off the arguments
of a 1-order logic formula abstracts to a propositional  logic  formula)
and to look first for a proof of this new formula. If a proof  is  found
here, it serves as a guideline for  a  proof  of  the  originally  given
formula.

YOUR TASK:
You should examine the applicability of these ideas  of  abstraction  to
our theorem prover and should implement them in this context.

Requirements:
At least, a master's degree in computer science, and some experience  in
automated theorem proving or being familiar with  the  "abstaction idea"
form some other point of view.

Duration:   summer '90
Wages:      competitive
Hours:      40h / week
 
Resume to:  B. Fronhoefer / R. Letz
            Tel. +49-89/521097 or 521098
            For the address, see location above, or
            e-mail: fronhoef@lan.informatik.tu-muenchen.dbp.de
 
------------------------------------------------------------------------
           S U M M E R  J O B
 
           Incorporating Equality into a Theorem Prover
 
Location:  Technical University Muenchen, West Germany
           AI research group
           Augustenstr. 46 RGB/II
           D-8000 MUENCHEN 2
 
Job Description:

Would you like to join us and help to extend our theorem prover ?

THE OVERALL PROJECT:
Durig the last years, we have developped a powerful theorem  prover.  It
is based on the model elimination calculus. High efficiency is gained by
compilation a la WAM. It compares well to other  international  research
projects. Current  research  interests  include  automated  learning  of
heuristics by a connectionistic approach.

SPECIFIC PROBLEM FIELD:
Incorporating  equality:  the  equality  relation  is   of   fundamental
importance in mathematics and computer science. Thus, there is a  strong
desire for efficient treatment as part of our theorem prover.  Our  work
so far: we have implemented a preprocessor, which incorporates  equality
into  a  logic  program.  The  preprocessor  includes   a   Knuth-Bendix
completion algorithm in order to compile a set of equations to a rewrite
system.

YOUR TASK:
If you like to, you can go on working in this field (e.g.  experimenting
and evaluating the potential of  completion,  developing  more  powerful
techniques than the current available ones).  We  are  open  minded  for
other approaches. For example, implementing a "standard" technique (e.g.
Paramodulation) would be interesting as well. Or do you  have  your  own
ideas of ...?

Requirements:
At least master's degree in computer science,  and  some  experience  in
automated theorem proving or related fields.

Duration:   summer '90
Wages:      competitive
Hours:      20 - 40 / week
 
Resume to:  P. Baumgartner
            Tel. +49-89/521098
            See location above, or
            e-mail: baumgarp@lan.informatik.tu-muenchen.dbp.de
************************************************************************