ECAI Conference 2002 Conference Paper
Automatic Learning in Proof Planning
- Mateja Jamnik
- Manfred Kerber
- Martin Pollet
Author name cluster
Martin Pollet
Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.
2 papers
1 author row
Possible papers
2LPAR Conference 2002 Conference Paper
Proof Development with Omega-MEGA: sqrt(2) Is Irrational
- Jörg H. Siekmann
- Christoph Benzmüller
- Armin Fiedler
- Andreas Meier 0002
- Martin Pollet
Abstract Freek Wiedijk proposed the well-known theorem about the irrationality of √2 as a case study and used this theorem for a comparison of fifteen (interactive) theorem proving systems, which were asked to present their solution (see [ 48 ]). This represents an important shift of emphasis in the field of automated deduction away from the somehow artificial problems of the past as represented, for example, in the test set of the TPTP library [ 45 ] back to real mathematical challenges. In this paper we present an overview of the Ωmega system as far as it is relevant for the purpose of this paper and show the development of a proof for this theorem.