@InProceedings{C1,
  key    =       {C01},
  author =	 {Christoph Benzm{\"u}ller and Lassaad Cheikhrouhou and Detlef Fehrer and
                  Armin Fiedler and Xiaorong Huang and Manfred Kerber and Michael Kohlhase
                  and Karsten Konrad and Erica Melis and Andreas Meier and Wolf
                  Schaarschmidt and J{\"o}rg Siekmann and Volker Sorge},
  title =	 {{OMEGA}: Towards a mathematical assistant},
  editor    = {William McCune},
  booktitle =	 {Automated Deduction - CADE-14, 14th International Conference
               on Automated Deduction, Townsville, North Queensland, Australia,
               July 13-17, 1997, Proceedings},
  publisher =	 {Springer},
  series =	 {LNCS},
  number =	 1249,
  pages =	 {252--255},
  year =	 1997,
  chrisnote =	 {C1},
  URL =		 {www.ags.uni-sb.de/~chris/papers/C1.pdf},
  abstract =	 {{Omega} is a mixed-initiative system with the ultimate purpose of
                  supporting theorem proving in main-stream mathematics and mathematics
                  education. The current system consists of a proof planner and an
                  integrated collection of tools for formulating problems, proving
                  subproblems, and proof presentation.}
}