####
Computer supported mathematics with ΩMEGA

*Jörg Siekmann
**
DFKI*

Universität des Saarlandes

###### Abstract

The year 2004 marks the fiftieth birthday of the first mathematical theorem to be proved by a
computer: "the sum of two even numbers is again an even number" (with Martin Davis'
imple-mentation of Presburger Arithmetic).
Classical theorem proving procedures of today are based on ingenious search techniques to find a
proof for a given theorem in very large search spaces - often in the range of several billion
clauses.

The shift from search based methods to more abstract planning techniques opened up a new para-digm
for mathematical reasoning on a computer and several systems of the new kind employ a mix of
classical as well as proof planning techniques.

In my talk I shall trace some key ideas of the past and then concentrate on current systems based
on proof planning, using ΩMEGA, a mathematical assistant system developed with the support of the
Sonderforschungsbereich 378 (Resource adapted cognitive Processes) as a case study for
demonstrating current strengths (and weaknesses) of the field.