@InProceedings{C12,
  key    =       {C12},
  author =	 {J\"org Siekmann and Christoph Benzm{\"u}ller and Armin Fiedler and Andreas Meier and
                  Martin Pollet},
  editor =       {Matthias Baaz and Andrei Voronkov}, 
  title =	 {Proof Development with {OMEGA}: Sqrt(2) is irrational},
  booktitle =	 {Logic for Programming, Artificial Intelligence, and Reasoning, 9th International Conference, LPAR 2002},
  year =	 2002,
  series =	 {LNCS},
  number =       2514,
  isbn =         3540000100,
  publisher =    {Springer},
  pages =        {367--387},
  url =		 {www.ags.uni-sb.de/~chris/papers/C12.pdf},
  CHRISNOTE =	 {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.}
}