Matroids Matheplanet Forum Index
Moderiert von mire2 StrgAltEntf
Mathematik » Logik, Mengen & Beweistechnik » Formalisierung von Gleichungsumformungen
Autor
Universität/Hochschule Formalisierung von Gleichungsumformungen
Finn0
Junior Letzter Besuch: im letzten Quartal
Dabei seit: 30.06.2021
Mitteilungen: 13
  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

Wechsel in ein anderes Forum:
 Suchen    
 
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2021 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]