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