The OMEGA System
OMEGA is a 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
Description
The project has been started by the Saarbrücken OMEGA Group, and has
since spread internationally.
OMEGA is a collection of software modules distributed
in the MathWeb network.
The OMEGA core runs on Allegro Common LISP
(together with it's object system CLOS). The graphical user interface
LOUI, which
you can run on-line over the Internet
See our primer for a hands-on tutorial.
Download & Installation
The OMEGA system is only available as a source distribution.
Selected Publications
-
OMEGA:
Towards a Mathematical Assistant, Conference on Automated Deduction 1997.
-
Integrating
Computer Algebra into Proof Planning M. Kerber, M. Kohlhase, V. Sorge. Journal of Automated
Reasoning 21(3) 1998
-
The Heine-Borel Challenge Problem: In Honor
of Woody Bledsoe. E. Melis. Journal of Automated Reasoning, 20(3), 1998.
-
A Blackboard Architecture for Guiding Interactive Proofs
Christoph Benzmueller and Volker Sorge, In:
Artificial Intelligence: Methodology, Systems and Applications, Proceedings of
the the 8th International Conference AIMSA'98, LNAI 1480, 1998.
- AI-Techniques in Proof Planning.
E. Melis, European Conference on Artificial Intelligence, 1998.
-
Knowledge-Based Proof Planning, E. Melis and J. Siekmann,
Artificial Intelligence, 115:65-105, 1999.
-
Extensions of Constraint Solving for Proof Planning , E. Melis and J. Zimmer and
T. Mueller, European Conference on Artificial Intelligence, 2000.
-
Proof Planning with Multiple Strategies, First International Conference on
Computational Logic, 2000.
designed by the OMEGA Group:
omega@ags.uni-sb.de
Last modified: Fri Oct 13 16:57:25 CEST 2006