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