|
|
|
|
|
![[Graphics:../Images/index_gr_4.gif]](../Images/index_gr_4.gif)
![[Graphics:../Images/index_gr_5.gif]](../Images/index_gr_5.gif)
![[Graphics:../Images/index_gr_6.gif]](../Images/index_gr_6.gif){kind=small}
![[Graphics:../Images/index_gr_7.gif]](../Images/index_gr_7.gif)
![[Graphics:../Images/index_gr_8.gif]](../Images/index_gr_8.gif){kind=small}
![[Graphics:../Images/index_gr_9.gif]](../Images/index_gr_9.gif)
![[Graphics:../Images/index_gr_10.gif]](../Images/index_gr_10.gif)
Computing + Solving + Proving
Natural-style questions: language of higher-order logic, 2D notation
Natural-style answers (proofs)
Still experimental
One logic and software frame for formal mathematics.
Combines automated reasoning with computer algebra.
A multi-method system. (Both general and special simplifiers, solvers, and provers in the system.)
An emphasis on "nice" input and output.
Programmed in Mathematica: platform independent. (However, no "hidden" knowledge of Mathematica is used!)
A joint effort of the Theorema Group at RISC, 1996-...: B. Buchberger, T. Jebelean, W. Windsteiger, K. Nakagawa, T. Kutsia, D. Vasaru, ...
Simple examples.
User view
![[Graphics:../Images/index_gr_11.gif]](../Images/index_gr_11.gif){kind=small}