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