Maxima

Maxima ist ein freies Computer-Algebrasystem (CAS), mit dem sich formale Mathematik betreiben lässt.

Das System wurde u.a. in Hugemann: Unfallrekonstruktion dazu genutzt, komplizierte Umformungen automatisch durchzuführen bzw. zu beweisen.

Besonders einfach ist es, die formale Identität zweier Ausdrücke f(x) und g(x) zu beweisen, weil dann in Maxima nur f(x) - g(x) zu berechnen ist, und das Ergebnis Null lauten sollte. Auf diese Weise wurden etwa sämtliche händischen Berechnungen von Pfeufer, H. zu seinem Buchbeitrag formal geprüft.

Auch im Colliseum wird an einigen Stellen Maxima-Code als Beweis für die Gültigkeit bestimmter Umformungen angegeben, so etwa unter Topokol.

Soweit man die Programmumgebung von Maxima nicht vollständig auf dem Rechner installieren möchte, kann man unter CESGA Maxima-Code online ausführen. (Wenn man möchte, sogar auch auf dem Smartphone.) Wie oft bei solche Weblösungen, ist die Version des Backends (Maxima) sehr alt. Größte praktische Hürde für den Ingenieur ist, dass Indizes wie in v₁ nicht als "v_1" geschrieben werden können, sondern als "v[1]" geschrieben werden müssen. (Und analog c[w] statt c_w, wo es dann krude wird.)

Hier der Code von der Seite Topokol in der »Online-Version« zum Copy-and-Paste in CESGA:

 impuls:mu*v[1] + v[2]=mu*vs[1]+vs[2];
 energie:mu*v[1]^2 +v[2]^2=mu*vs[1]^2+vs[2]^2+mu/(1+mu)*ve^2;
 Loesung:algsys([impuls,energie],[v[1],v[2]]);
 Loesung[2][1];
 facsum(solve(impuls,v[2])[1],mu);