## Jörg Siekmann, Michael Kohlhase and Erica Melis

FB Informatik

Universität des Saarlandes

D-66041 Saarbrücken

Germany

siekmann@cs.uni-sb.de,
http://www.ags.uni-sb.de/~siekmann

kohlhase@cs.uni-sb.de,
http://www.ags.uni-sb.de/~kohlhase

melis@cs.uni-sb.de,
http://www.ags.uni-sb.de/~melis

### Abstract

Classical automated theorem provers can prove non-trivial mathematical theorems
in highly specific settings. However they are generally unable to cope with
even moderately difficult theorems in mainstream mathematics. While there are
many reasons for the failure of the classical search-based paradigm, it is
apparent that mathematicians can cope with long and complex proofs and have
strategies to avoid less promising proof paths without suffering from the
exponential search spaces. Consequently, a combination of the power of
automated tools with human-like capabilities seems necessary to prove
main-stream mathematical theorems with the help of a machine. In the following,
we shall describe the prototypical system OMEGA that explores proof planning
together with high-level proof tools. OMEGA is a mixed-initiative system with
the ultimate goal of supporting theorem proving in main-stream mathematics and
mathematics education.

Dvi-file

PS-File

PDF-File

Bibtex Entry