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.

sfb-logo Zur Startseite Erstellt von: Anke Weinberger (2005-10-28).
Wartung durch: Anke Weinberger (2005-10-28).