Ωmega: Computer supported mathematics

Abstract

The year 2004 marks the fiftieth birthday of the first computer generated proof of a mathematical theorem: "the sum of two even numbers is again an even number" (with Martin Davis' implementation of Presburger Arithmetic in 1954). While Martin Davis and later the research community of automated deduction used machine oriented calculi to find the proof for a theorem by automatic means, the Automath project of N.G. de Bruijn http://www.win.tue.nl/ automath/ - more modest in its aims with respect to automation - showed in the late 1960s and early 70s that a complete mathematical textbook could be coded and proof-checked by a computer. 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. But in spite of many successful attempts to prove even open mathematical problems automatically, their use in everyday mathematical practice is still limited. The shift from search based methods to more abstract planning techniques however opened up a new paradigm for mathematical reasoning on a computer and several systems of the new kind now employ a mix of interactive, search based as well as proof planning techniques. The Ωmega system is at the core of several related and well-integrated research projects of the Ωmega research group, whose aim is to develop system support for the working mathematician, in particular it supports proof development at a human oriented level of abstraction. It is a modular system with a central proof data structure and several supplementary subsystems including automated deduction and computer algebra systems. Ωmega has many characteristics in common with systems like NuPrL [ACE+00], CoQ [Coq03], Hol [GM93], Pvs [ORR +96], and Isabelle [Pau94,NPW02]. However, it differs from these systems with respect to its focus on proof planning and in that respect it is more similar to the proof planning systems Clam and λClam at Edinburgh [RSG98,BvHHS90]. © 2004 Springer-Verlag.