Universität des Saarlandes
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.
Erstellt von: Anke Weinberger (2005-10-28).
Wartung durch: Anke Weinberger (2005-10-28).