C/C++ symbolische Mathematik beibringen...
-
Eine große Schwierigkeit ist es auch, jeden Ausdruck auf eine kanonische Form zu bringen (d.h. gleiche Ausrücke auch als gleich zu erkennen.
-
Winn schrieb:
Gute Begriffe, Links, Bücher... wenn ihr was wißt, bitte, her damit.
keine ahnung. aber für mich wäre der naheliegende weg, nen lisp-interpreter in c++ zu implementieren (und die klassen würde ich xlisp nennen, wenn es xlisp nicht schon gäbe. vielleicht auch lisp plus plus (tip!)) und den gleichungslöser dann in lisp bauen.
-
Matrizen sind was für 3D Spiele. Jede gute Spiele Engine kapselt eine Klasse die mit Matrizen rechnen kann. Aber jede x beliebige Formel lösen, geht nur, wenn die Formel mit vielen vielen case Anweisungen zerlegt und analysiert wird.Für jede Möglichkeit muß dann eine andere Methode aufgerufen werden die das Ganze ausrechnet. Alles nur viel Fleissarbeit. Mathematik ist logisch und so lassen sich auch alle Gesetzte in Programm packen. Aber dafür ist bereits reichlich Anwendersoftware erstellt die auch bestens funktioniert.
-
Genau! Und deswegen lernen Informatiker im Studium fast nur 10-FingerSystem, damit sie nachher schnell tippen können! Möglicherweise dann auch in Partnerarbeit, so mit 20 Fingern!
Mal im Ernst: glaubst Du wirklich, daß die sich bei z.B. Maple hingesetzt haben und das ganze mit switch-case analysiert haben und jeden einzelnen Fall einzeln implementiert haben? Nicht? Ich auch nicht. Sowas macht man mit allgemeinen Regeln, die man zum Beispiel in Prädikatenlogik oder ähnlichem kodiert. Die läßt man dann vom Rechner anwenden. Das einzige was man wirklich programmieren muß ist ein kleiner Parser, ein Term-Matcher und einen ordentlichen Suchalgorithmus mit ner guten Heuristik.
MfG Jester
-
@Jester
ich glaube er weiss einfach absolut nicht wo von er spricht.
-
Jester schrieb:
Mal im Ernst: glaubst Du wirklich, daß die sich bei z.B. Maple hingesetzt haben und das ganze mit switch-case analysiert haben und jeden einzelnen Fall einzeln implementiert haben? Nicht? Ich auch nicht.
Ich auch nicht. Allerdings habe ich vor einiger Zeit festgestellt, dass mir bei so simpel erscheinenden Dingen, wie dem Vereinfachen von mathematischen Termen, einfach keine allgemeine Herangehensweise einfällt. Wie geht man da ran, ohne massenhalft sehr spezielle Regeln aufzustellen, die man dann mit ifs oder ähnlichen Dingen nacheinander abhakt.
Hier mal ein Auszug aus einer Klasse MulFunction, die ich vor längerer Zeit mal geschrieben habe. Ich hoffe, mein Problem (bzw. meine offensichtlich falsche Herangehensweise) wird dadurch klar. Die Klasse ist wäre nach dieser Art natürlich noch lange nicht fertig. Eigentlich müßten da dann noch etliche weitere Regeln rein.
@Override public final Function getSimplifiedFunction() { List<Function> functionList = new LinkedList<Function>(); for (final Function function : getFunctionList()) functionList.add(function.getSimplifiedFunction()); functionList = simplifyMulFunctions(functionList); functionList = simplifyConstFunctions(functionList); functionList = simplifyEqualFunctions(functionList); Function tempFunction = simplifyDivisionFunctions(functionList); if (tempFunction != null) return tempFunction.getSimplifiedFunction(); // ToDo if (functionList.size() == 0) return ConstFunction.ONE; if (functionList.size() == 1) return functionList.get(0); return new MulFunction(functionList.toArray(new Function[0])); } private static List<Function> simplifyConstFunctions(final List<Function> functionList) { double value = 1.0; final Iterator<Function> iterator = functionList.iterator(); while (iterator.hasNext()) { final Function function = iterator.next(); if (function instanceof ConstFunction) { value *= ((ConstFunction)function).getValue(0); iterator.remove(); } } if(value == 0.0) { functionList.clear(); functionList.add(ConstFunction.ZERO); } if(value != 1.0) functionList.add(ConstFunction.valueOf(value)); return functionList; } private static List<Function> simplifyMulFunctions(final List<Function> functionList) { final List<Function> outList = new LinkedList<Function>(); for (final Function function : functionList) { if (function instanceof MulFunction) { final List<Function> tempFunctions = simplifyMulFunctions(((MulFunction)function).getFunctionList()); for (final Function tempFunction : tempFunctions) outList.add(tempFunction); } else { outList.add(function); } } return outList; } private static Function simplifyDivisionFunctions(final List<Function> functionList) { final List<Function> dividendList = new LinkedList<Function>(); final List<Function> divisorList = new LinkedList<Function>(); for (final Function function : functionList) { if (function instanceof DivisionFunction) { final DivisionFunction divFunction = (DivisionFunction) function; dividendList.add(divFunction.getDividend()); divisorList.add(divFunction.getDivisor()); } else { dividendList.add(function); } } if(divisorList.size() == 0) return null; final MulFunction dividend = new MulFunction(dividendList.toArray(new Function[0])); final MulFunction divisor = new MulFunction(divisorList.toArray(new Function[0])); return new DivisionFunction(dividend,divisor); } private static List<Function> simplifyEqualFunctions(final List<Function> functionList) { final List<Function> outList = new LinkedList<Function>(); while(functionList.size() != 0) { Iterator<Function> iterator = functionList.iterator(); final Function function = iterator.next(); iterator.remove(); final List<Function> sumList = new LinkedList<Function>(); sumList.add(ConstFunction.ONE); while (iterator.hasNext()) { final Function currentFunction = iterator.next(); if (function.equals(currentFunction)) { iterator.remove(); sumList.add(ConstFunction.ONE); } else if(currentFunction instanceof PowerFunction) { final PowerFunction powerFunction = (PowerFunction) currentFunction; final Function base = powerFunction.getBase(); if (function.equals(base)) { sumList.add(powerFunction.getExponent()); iterator.remove(); } } } final Function[] sumFunctions = sumList.toArray(new Function[0]); if (sumFunctions.length > 1) { outList.add(new PowerFunction(function,new SumFunction(sumFunctions)).getSimplifiedFunction()); } else outList.add(function); } return outList; }
-
CRIUIX schrieb:
Mathematik ist logisch und so lassen sich auch alle Gesetzte in Programm packen.
Du solltest dich von der Vorstellung lösen, dass die Mathematik nach den Potenzgesetzen aufhört
.
-
@Gregor: Kannst Du vielleicht kurz erklären, was die Klasse genau macht? Ich steig ehrlich gesagt nicht so ganz durch.
Mein Ansatz wäre folgender:
m(x,y) ist das Produkt von x,y. Jetzt kann ich in Zum Beispiel Prädikaten logik folgende Axiome formulieren.
Für alle x,y: m(x,y) = m(y,x) // Kommutativität
Für alle x,y,z: m(m(x,y),z) = m(x,m(y,z)) // Assoziativität
Für alle x: x!=0 => m(x,i(x)) = 1 // Inverse
Für alle x: m(x,1) = x // 1 neutraletc. solche Axiome auch für Addition.
Dann brauchst Du einen Parser, der einen Term in einen solchen Ausdruck umwandelt und eine Funktion, die alle anwendbaren Regeln findet. Damit kannst Du das ganze im Prinzip als Suche auffassen. Du hast Deinen Ausgangspunkt gegeben und Du kennst die möglichen Schritte, also kannst Du nen Suchbaum aufspannen. Was Dir noch fehlt ist ein guter Zieltest, ob Du bereits fertig bist mit vereinfachen, sowie ne gute Heuristik, die sagt welche Schritte Du anwenden solltest. Vielleicht sind Schritte, die die Termlänge verkürzen besser als andere... oder sowas in der Art.
Um auch Konstanten zusammenfassen zu können, könntest Du die Verarbeitung von sowas wie m(4,5) nicht durch den normalen Algorithmus behandeln lassen, sondern duch eine selbsgebaute Funktion, die das ganze einfach ersetzt.MfG Jester
-
Jester schrieb:
@Gregor: Kannst Du vielleicht kurz erklären, was die Klasse genau macht? Ich steig ehrlich gesagt nicht so ganz durch.
Das ist da ja auch nur ein kleiner Ausschnitt der Klasse.
Bei mir bilden Funktionen so eine Art Baumstruktur. Diese Klasse MulFunction steht hierbei für eine Funktion, die mehrere andere Funktionen miteinander multipliziert, also in etwa so ein Ding:
f(x) = g(x) * h(x) * i(x).
Die kann natürlich oft vereinfach werden. Das einfachste Beispiel wäre, wenn z.B.
h(x) = 0
gelten würde.
Dann würde f(x) zu f(x) = 0 vereinfacht werden. Wenn h(x) stattdessen 1 wäre, dann würde f(x) zu f(x) = g(x) * i(x) vereinfacht werden. Um diese Art von Vereinfachungen geht es mir. Die Art, wie ich es mache, scheint mir sehr aufwändig zu sein. Ich frage mich halt, ob man solche Vereinfachungen nicht irgendwie auf sehr wenige Regeln zurückführen kann. Was wäre zum Beispiel, wenn ich eine Funktion f(x) = sin²(x) + cos²(x) hätte. Muss man da explizit eine Regel angeben, dass das 1 ist, oder kann man das auch eleganter lösen?
Auf der Ebene, auf der ich diese Funktionen (oder Terme) momentan betrachte, gibt es einfach viel zu viele Regeln, die zu einem unglaublich riesigen, schlecht wartbaren Codeberg führen würden, wenn man die konsequent alle einprogrammiert.
Eine zweite Sache ist die Repräsentation von solchen Regeln. Wie macht man das und wo macht man das am Besten. Java scheint mir nicht gerade eine ideale Sprache zu sein, um solche Regeln damit zu repräsentieren. ...C++ genausowenig. Welche Sprache wäre dafür geeignet? Prolog? ...oder sollte man die zur Laufzeit zum Beispiel aus einer XML-Datei oder so in eine geeignete Datenstruktur einlesen und damit arbeiten?
-
Also ich denke Prolog wäre sehr geeignet um solche Regeln zu formulieren. Es gibt meines Wissens auch eine Schnittstelle zwischen Prolog und C++.
-
Ja, Prolog könnte eine Lösung sein. Ich weiß aber nicht, wie gut Prolog mit Gleichheiten umgehen kann. Die sind in der Logik grundsätzlich etwas eklig, weil sie nicht so schön mit sich Arbeiten lassen, wie Implikationen. Man hat grundsätzlich 2 Richtungen, und dadurch, daß sich die ganzen Funktionsausdrücke schachteln lassen erhält man stets einen unendlich großen Suchraum.
Zum Ausdrücken der Regeln eignet sich wie gesagt die Prädikatenlogik sehr gut. Allerdings wirste auf Grund der oben genannten Probleme ne gute Heuristik brauchen, nach der Du die Regeln anwendest, sonst wird der Suchraum zu groß.
Die Variablen x,y,z müssen keine einzelnen Zahlen sein, sondern können selbst wieder komplexe Ausdrücke sein.Eine Möglichkeit wäre, die Gleicheiten nur von links nach rechts zuzulassen. Das ist wohl die häufigste Benutzung. Leider muß man dann manche Sachen explizit angeben:
Zum Beispiel beim ausklammern:
Für alle x,y,z:
add(mul(x,y),mul(x,z)) = mul(x,add(y,z))Man beachte, daß aufgrund der Kommutativität der Beweiser jetzt schon ganz allegemein ausklammern kann. Er muß nur auf die Idee kommen alles nach vorne zu schieben was gemeinsam ist.
wenn wir jetzt m(x,1) = x nur von rechts nach links verwenden, dann kann der Beweiser add(x,x) nicht vereinfachen. Lassen wir auch die andere Richtung zu, so kann er daraus add(m(x,1),m(x,1)) machen und daraus m(x,add(1,1)) machen und daraus dann mit Hilfe einer speziellen Rechenprozedur außerhalb der Prädikaten logik mul(x,2).
Der Vorteil der Darstellung in Prädikatenlogik ist, daß man auch Aussagen über Funktionen treffen kann, die nicht definiert sind:
Für alle x: sin(add(x,mul(2,Pi))) = sin(x) besagt, daß sin 2Pi periodisch ist. Die Additionstheoreme kann man genauso einfach angeben und schon kann er mit sin+cos rechnen. Ein paar Axiome zu exp und dann kann er das auch.
Weiterhin ist es problematisch die richtigen Einsetzungen in die Regeln zu finden:
mul(add(mul(a,a),neg(mul(b,b)), i(add(a,b))
das ist (a2-b2)/(a+b)
wenn der Computer jetzt auf die Idee käme ein paar Axiome anzuwenden, wie:
(I) für alle x: add(x,0) = x
(II) für alle x: add(x,neg(x)) = 0dann könnte er daraus folgendes machen:
(I) => mul(add(add(mul(a,a),neg(mul(b,b)), 0), i(add(a,b))
(II) => mul(add(add(mul(a,a),neg(mul(b,b)),add(mul(a,b),neg(mul(a,b)), i(add(a,b))Das heißt: a2-b2 = a2-b2 + 0 = a2-b2 + ab - ab jetzt das Kommutativ und assoziativgesetz der Addition:
a^2+ab - ab - b^2 jetzt bemerkt er, daß sein Distributgesetz greift:
a(a+b) - b(a+b)
jetzt noch a+b ausklammern und fertig.
Nur, wie kommt der Rechner auf die Idee? Wenn man ihm so viel Zeit läßt diesen Weg zu finden, dann braucht man entweder ne sehr gute Heuristik, die dem Rechner sagt: da gibt's was zu holen, oder alternativ kann man natürlich auch einfach die binomischen Formeln in Prädikatenlogik formulieren. Das ist zwar redundant, aber effektiv und spart dem Rechner das raten welche Variablen er dazu erfinden muß.In vielen Fällen ist das wohl einfacher.
Man kann leicht zeigen, daß für alle x: x= i(i(x))x = mul(x,1) = mul(x, mul(i(x), i(i(x)) = mul(mul(x,i(x)), i(i(x)) = mul(1,i(i(x)) = i(i(x)), aber der Rechner würde wahrscheinlich lange brauchen. Also geben wir ihm vielleicht auch noch diese Info. Ähnlich ist es mit für alle x: mul(0,x) = 0.
Dennoch kann man mit einer ausreichend großen Regelmenge gute Ergebnisse erreichen.
MfG Jester
-
zuerst hat mich ein lehrer gelernt, daß ich (a+b)^2 immer zu a2+2ab+b2 vereinfachen soll. binomische formel heißt das.
und kaum drei jahre später (oder waren es eher 10?) meint einer, ich solle a2+2ab+b2 zu (a+b)^2 vereinfachen.
ja, was denn nu? und wie soll ich dem bot was beibringen, was ich selber nicht weiß?
soll ein matheprogramm zu a2+2ab+b2 oder zu (a+b)^2 vereinfachen?
-
Ich finde (a+b)^2 schöner. Eben, weil man da auch (a+b) kürzen kann. Ein Schritt, der einem sonst durch die Lappen geht. Aber man muß natürlich irgendwie definieren, wann ein Term einfacher ist als ein anderer.
MfG Jester
-
@Jester & Gregor:
Die Sache mit der Prädikatenlogik hört sich bis hierher gut anObwohl ich jetzt, beim ersten flüchtigen durchlesen des Threads, nicht
ganz hinter die Logik steige. Ich werde mir die Beiträge nochmal durchlesen
müssenAber:
Geht das mit der Prädikatenlogik bis zum Letzten? Also ich denke jetzt mal
an meine Mathematik I + II Vorlesungen. Alleine schon die recht einfache
Integration und Differentiation über eine Veränderliche ist "harter Tobak".Ich meine: Man kann ihm sagen:
Das ist die Kettenregel, dass die Summenregel etc.Das ist noch kein Problem. Aber wenn es dann um die partielle Integration
geht, oder die Integration durch Substitution etc.Das Programm muss ja selbst erkennen, wann es durch Substitution Integriert,
und wann durch partielle Integration oder in welchen Fällen lieber elementar.Aber wenn so ein Programm an Mathematica oder Maple heran kommen soll, muss
man noch viel viel mehr können:Wie sieht es mit Integration von mehreren Veränderlichen aus? Da fängt der
Spaß doch erst an :p Kurvenintegrale, Oberflächenintegrale, Volumenintegrale,
Bereichsintegrale etc. pp.Differentialgleichungen n-ter Ordnung
Da gibt es zum Beispiel den speziellen Funktionsansatz für die inhomogene
Lösung einer Differentialgleichung 2. Ordnung. Das ist ne Tabelle zum
nachschlagen. Soll das Programm die Tabelle beinhalten? Wohl eher nicht...Dann muss man dem Programm den Differentialoperator beibringen. Wenn es
das kann, kann man Taylerreihenentwicklung mit mehreren Veränderlichen
durchführen.Fourierreihenentwicklung ist auch nicht ohne
Wie kann die Software
die Sonderfälle erkennen, wie gerade / ungerade Funktion? Okay, dass
könnte sie ja schon. Alternierende Funktionen erkennen... hmmm.Wie sieht es mit komplexen Zahlen aus? Das müsste die Software schaffen,
wenn sie das i bzw. j kapiert hat. Okay, dann braucht man aber auch
eine Erkennung, wann die Software in die Exponentialform wechselt.
Also sobald andere Operationen als Addition oder Subtraktion auftauchen,
immer in die Exponentialform gehen...Aber wie will man Sachen erkennen, wie die Vereinfachungen bei der
Integration mehrerer Veränderlicher? Die Koordinatentransformation zum Beispiel.
Wie soll die Software erkennen, dass der zu berechnende Körper eine
Zylinderform hat? Dann muss sie nämlich eine Koordinatentransformation
in die Zylinderkoordinaten durchführen etc.Das ist alles ne Menge Arbeit. Ich hatte auch schonmal die Idee, sowas
zu programmieren (in Java). Aber bei den Überlegungen kommt man zu vielen
Problemen.Aber wie gesagt: Prädikatenlogik hört sich zumindest für den einfachen
Teil der Mathematik gut an.Ich hatte natürlich auch schonmal nachgeforscht, wie das Andere machen.
Ich habe einen interessanten Ansatz der FH Wedel gefunden:
http://www.fh-wedel.de/~si/praktika/MultimediaProjekte/MathApplet/doc/umsetzung.htmlDas wäre doch ne gute Idee.
So ein Programm wäre dann sogar ziemlich übersichtlich! Man hätte ja eine
Klasse pro Operator. Und das scheint ja auch zu funktionierenWäre ein schönes Projekt. Wollt ihr das wirklich programmieren? Wäre ja
coolDa gibt es auch noch andere Probleme:
Die Formelzeichen müssen dynamisch gezeichent werden. Ein Wurzelzeichen
muss sich dem Ausdruck anpassen. Man muss Integrale unter Bruchstrichen,
und das wieder in Wurzeln packen können usw.Das muss man auch alles hinbekommen
wobei das gegen das
Mathematik-Modell dahinter vergleichber einfach ist...
-
Rein theoretisch müßte der Rechner sogar selbst die partielle Integration herleiten können. Das Problem ist, wie Du richtig festgestellt hast eine gute Heuristik zu haben, um zu wissen, welche Regelanwendungen Erfolg versprechen. Vielleicht könnte man den Ausdruck erstmal grob analysieren und dann sagen, okay, dieses Bündel an Regeln dürfte am meisten bringen, und dann arbeitet man mit einer Untermenge weiter. Integrale mit exp oder trigonometrischen Funktionen lassen sich gern mit partieller Integration lösen. Viele eindimensionale Integrationsprobleme lassen sich mit Standardsubstitutionen lösen. Man muß nur rausfinden von welchem Typ sie sind.
Auch die Prädikatenlogik 1.Ordnung ist nicht ganz ausreichend um alles mathematische auszudrücken. Dennoch ist sie schon so umfangreich, daß sie unentscheidbar ist. Man kann also letztlich nicht immer entscheiden, ob eine gegebene Aussage wahr oder falsch ist. Das Problem ist also sehr hart. Deswegen muß man hier sowieso mit Näherungen arbeiten.
In der Prädikatenlogik 1. Ordnung kann man ja nur über Variablen quantifizieren. Damit läßt sich sowas wie Induktion aber nicht durchführen. Dafür müßte man nämlich auch über Prädikate Quantifieren können:
etwa so:
Für alle Prädikate P: (P(0) und (P(n) => P(n+1))) => Für alle n: P(n)
Das ist +/- das 5. Peano-Axiom. In reiner Präd.-Log. 1. Ordnung ließe es sich nicht formulieren. Allerdings ist automatisches Beweisen in Logiken höherer Ordnung noch viel schwerer. In der Prädikatenlogik gibt's immerhin noch korrekte vollständige Algorithmen: Das heißt, gefundene Beweise sind korrekt und wenn ein Beweis existiert, so wird er auch gefunden. Sowas ist in höheren Ordnung meines Wissens nicht mehr gegeben. Es ist aber auch fraglich, ob der Rechner wirklich ne Induktion machen muß.MfG Jester
-
Aber dreht man sich nicht im Kreis:
Ich kann mit der Prädikatenlogik alleine nichts machen, weil die Heuristik
zunächst eine Entscheidung treffen muss.Nun gut.
Aber die Heuristik muss dazu das "Wissen" der Mathematik haben -- also braucht
sie wiederum die Prädikatenlogik. Wenn die Heuristik die Regeln kennen und
können muss, dann brauchen wir ja keine Prädikatenlogik mehr. Oder?
-
Die Heuristik ist oberflächlicher und ungenauer.
Wenn Du Dir nen komplexen Term anschaust und den vereinfachen willst, dann weißt Du nicht sofort was rauskommt (zumindest bei mir isses so), aber es fallen einem sofort gewisse Rechenregeln ein, die was bringen *könnten*, nicht müssen(!). Und mit diesen probierst Du dann rum um es einfacher zu kriegen.Und wenn jetzt unser Programm durch ansehen des Terms zumindest abschätzen kann, welche Rechenregeln zur Vereinfachung führen könnten, dann machen wir damit den Suchraum drastisch kleiner, weil sämtliche Regeln, die eh nix bringen aussortiert sind. Das Problem ist ja nicht, daß wir zu wenig Ausdruckskraft hätten mit der PL1, sondern daß wir soviel sagen können, daß der Suchraum riesig wird.
MfG jester
-
Okay. Das ist aber zunächst im ersten Schritt nicht so schwer
Sagen wir mal zunächst, dass wir für jede Regel eine Klasse haben. Oder zumindest
eine Klasse pro Regel-Typ. Also eine Klasse für Integration, Grundrechenarten usw.Dann würde die Heuristik die gegebenen Daten analysieren:
- Ist eine Zeichenfolge "int" vorhanden? Ja --> Integration vormerken
- Ist ein "+", "-", "*" oder "/" Zeichen vorhande? Ja --> Grundrechenarten vormerken
- Ist ein "/"-Zeichen vorhanden? Bruchrechnung vormerken
- Ist ein "(" oder ")" vorhanden? .... etc.
Damit kann man ganz ganz grob aufteilen, was man ganz sicher nicht braucht.
Als Symbole für Integral etc. könnte man sich auf die LaTeX-Befehle einigen.
Zumindest, wenn es Sinn macht.Tja... dann geht es schon los, die Feinheiten zu suchen
Und dann wirds
schwerEine Idee wäre:
Man würde eine Klasse mathParser basteln, die abstrakt ist. Sie kann also
nicht instanziert werden. Von ihr erben alle Rechenarten etc.Dann könnte man zum Beispiel beim ersten Auftreten von "(" das passende
")" Zeichen suchen. Diesen Teil-String gibt man dem Konstruktor der
brackets-Klasse mit. Dieser ruft wieder den Parser auf (den hat er ja
geerbt) und der Parser analysiert den Rest des Teil-Strings.Dadurch würde sich doch automatisch eine Art Tree-Struktur ergeben.
Wo speichert man die Referenzen (Zeiger) auf die Objekte? Man könnte
eine Singleton-Klasse haben, die in einem Array oder (in Java) in einer
ArrayList die Instanzen bewart.
Oder man bastelt sich etwas ähnliches, wie in dem Link den ich angegeben
hatte. Jedes Objekt hat eine Methoe hasNextNote() etc. Dann würe man
eine neue Instanz einer Klasse in dem Objekt speichern, die das neue
Objekte angelegt hat
-
-- Trigonometrische Funktionen auf exp zurückführen.
-- Universalsubstitution tan(x/2)
-- Paradigms of Artificial Intelligence Programming, http://www.norvig.com/paip/README.html
-
Meine laienhaften Vorstellungen zu dem Thema: Es muss doch "nur" möglich sein, dass ein Programm einen normierten Term bewerten kann und dann aus einem Katalog ermittelt welche Regeln Anwendung finden könnten und eine Art Brute-Force startet bis das gewünschte Ergebnis erzielt wurde. Natürlich muss es ein guter Algorithmus sein, denn sonst probiert er u.U. zemlich lange herum. Auch müssen geeignete Abbruchbedingungen vorliegen (z.B. Abbruch wenn die Umformung wieder einen Ursprungsterm ergibt).