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
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.