OMEGA: Towards a mathematical assistant (bibtex)
by Christoph Benzmüller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Karsten Konrad, Erica Melis, Andreas Meier, Wolf Schaarschmidt, Jörg Siekmann, Volker Sorge
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.
Reference:
OMEGA: Towards a mathematical assistant (Christoph Benzmüller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Karsten Konrad, Erica Melis, Andreas Meier, Wolf Schaarschmidt, Jörg Siekmann, Volker Sorge), In Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings (William McCune, ed.), Springer, LNCS, number 1249, pp. 252-255, 1997. (Url (preprint): http://christoph-benzmueller.de/papers/C1.pdf)
Bibtex Entry:
@inproceedings{C1,
  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.},
  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},
  Booktitle =	 {Automated Deduction - CADE-14, 14th International
                  Conference on Automated Deduction, Townsville, North
                  Queensland, Australia, July 13-17, 1997,
                  Proceedings},
  Doi =		 {10.1007/3-540-63104-6_23},
  Editor =	 {William McCune},
  Keywords =	 {own, Proof Assistants, OMEGA, Interactive Proof,
                  Automated Reasoning, Proof Planning, System
                  Integration},
  Number =	 1249,
  Pages =	 {252-255},
  Publisher =	 {Springer},
  Series =	 {LNCS},
  Title =	 {{OMEGA}: Towards a mathematical assistant},
  Note =	 {Url (preprint):
                  \url{http://christoph-benzmueller.de/papers/C1.pdf}},
  Year =	 1997,
}
Powered by bibtexbrowser