| |
| Autor |
 Formalisierung von Gleichungsumformungen |
|
Finn0
Aktiv 
Dabei seit: 30.06.2021
Mitteilungen: 55
 |  Themenstart: 2021-10-25
|
Gegeben sei die Gleichung $x+1=2$. Zu bestimmen ist ihre Lösungsmenge. Allerdings möchte ich ausschließlich formalisierte Schlussfolgerungen benutzen, die man auch im Computer implementieren kann. Meine Frage ist, wie man das am elegantesten bewerkstelligt.
Grundlagen wie Prädikatenlogik, Substitution freier Variablen, Compilerbau und Unifizierung sind mir ein Begriff. Das darf als bekannt vorausgesetzt werden.
Ich habe mir überlegt, es wird definiert:
$\text{Axiom add}, \vdash \forall a,b,c\colon (a=b\iff a+c=b+c)$
$\text{Axiom add_al}, \vdash \forall a,b,c\colon (a+b)+c = a+(b+c)$
$\text{Axiom add_neut}, \vdash \forall a\colon a+0 = a$
Außerdem sei ein Evaluator ev gegeben.
Man kann nun wie folgt schlussfolgern.
$\text{add}(a:=x+1, b:=2, c:=-1)$
1. $\vdash x+1 = 2 \iff (x+1)+(-1) = 2 + (-1)$
$\text{add_al}(a:=x,b:=1,c:=-1)$
2. $\vdash (x+1)+(-1) = x + (1+(-1))$
Nun steht man vor dem Problem, dass man in einen Ausdruck rein muss. Da könnte man Pattern matching machen lassen, was aber keine allgemeine Lösung darstellt. Stattdessen führe ich explizit Hilfsvariablen ein, so dass der Ausdruck nach Substitution mit einem bereits gefundenen übereinstimmt.
Hilfsvariablen für 1.
3. $\vdash x+1 = 2 \iff a = b, \quad a:=(x+1)+(-1),\quad b := 2+(-1)$
Zu 3. $\mathrm{eq}(a,2.), \mathrm{ev}(b)$
4. $\vdash x + 1 = 2\iff a = b, \quad a:=x+(1+(-1)),\quad b:=1$
Expandiere 4.
5. $\vdash x + 1 = 2\iff x+(1+(-1)) = 1$
Hilfsvariable für 5.
6. $\vdash x + 1 = 2\iff x+a = 1,\quad a:=1+(-1)$
Zu 6. $\mathrm{ev}(a)$
7. $\vdash x + 1 = 2\iff x+a = 1,\quad a:=0$
Expandiere 7.
8. $\vdash x + 1 = 2\iff x+0 = 1$
Hilfsvariable für 8.
9. $\vdash x + 1 = 2\iff t = 1,\quad t:=x+0$
$\text{add_neut}(a:=x)$
10. $\vdash x+0=x$
Zu 9. $\mathrm{eq}(t,10.)$
11. $\vdash x + 1 = 2\iff t = 1,\quad t:=x$
Expandiere 11.
12. $\vdash x + 1 = 2\iff x = 1$
Mir ist das zu kompliziert. Eine erste Vereinfachung wäre, den Evaluator auf Terme mit Variablen anwenden zu können und ihn nebenbei auf den gesamten Term loslassen zu können. Mit weiteren Hilfsvariablen kann man Abkürzungen einführen. Allerdings erhöht jede Hilfsvariable potenziell die kognitive Komplexität.
Hat noch jemand Ideen, ob es eine alternative Vorgehensweise gibt, oder wie man die Vorgehensweise verbessern kann?
Ein weiteres Ziel ist, dass ein CAS diesen Trace automatisch produziert und der Beweisassistent den anschließend verifiziert.
|
 Profil
|
|
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2023 by Matroids Matheplanet
This web site was originally made with PHP-Nuke, a former web portal system written in PHP that seems no longer to be maintained nor supported. PHP-Nuke is Free Software released under the GNU/GPL license.
Ich distanziere mich von rechtswidrigen oder anstößigen Inhalten, die sich trotz aufmerksamer Prüfung hinter hier verwendeten Links verbergen mögen.
Lesen Sie die
Nutzungsbedingungen,
die Distanzierung,
die Datenschutzerklärung und das Impressum.
[Seitenanfang]
|
Home / Seite ohne Frame
Wie unterstütze ich den Matheplaneten mit Geld?
