Proof Development with OMEGA: Sqrt(2) is irrational (bibtex)

by Jörg Siekmann, Christoph Benzmüller, Armin Fiedler, Andreas Meier, Martin Pollet

Abstract:

Freek Wiedijk proposed the well-known theorem about the irrationality of sqrt2 as a case study and used this theorem for a comparison of fifteen (interactive) theorem proving systems, which were asked to present their solution. 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 back to real mathematical challenges. In this paper we present an overview of the OMEGA system as far as it is relevant for the purpose of this paper and show the development of a proof for this theorem.

Reference:

Proof Development with OMEGA: Sqrt(2) is irrational (Jörg Siekmann, Christoph Benzmüller, Armin Fiedler, Andreas Meier, Martin Pollet), In Logic for Programming, Artificial Intelligence, and Reasoning, 9th International Conference, LPAR 2002 (Matthias Baaz, Andrei Voronkov, eds.), Springer, LNCS, number 2514, pp. 367-387, 2002. (slides) (Url (preprint): http://christoph-benzmueller.de/papers/C12.pdf)

Bibtex Entry:

@inproceedings{C12, Abstract = {Freek Wiedijk proposed the well-known theorem about the irrationality of sqrt{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. 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 back to real mathematical challenges. In this paper we present an overview of the OMEGA system as far as it is relevant for the purpose of this paper and show the development of a proof for this theorem.}, Author = {J\"org Siekmann and Christoph Benzm{\"u}ller and Armin Fiedler and Andreas Meier and Martin Pollet}, Booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 9th International Conference, LPAR 2002}, Comment = {<a href="http://christoph-benzmueller.de//papers/2002-lpar.pdf">slides</a>}, Editor = {Matthias Baaz and Andrei Voronkov}, Isbn = 3540000100, Keywords = {own, Proof Assistants, OMEGA, Interactive Proof, Automated Reasoning, Proof Planning, System Integration}, Number = 2514, Pages = {367-387}, Publisher = {Springer}, Series = {LNCS}, Title = {Proof Development with {OMEGA}: Sqrt(2) is irrational}, Note = {Url (preprint): \url{http://christoph-benzmueller.de/papers/C12.pdf}}, Year = 2002, }

Powered by bibtexbrowser