Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Prädikatenlogik, Deduktion, Hoare Kalkül - Was ist was?
Hallo miteinander,
ich studiere im 1. Semester Wirtschaftsinformatik und bin grad dabei eine Vorlesung (Mathematik für Informatiker) nochmal nach zu arbeiten…
…wollte mal fragen, ob mir jemand vielleicht die Seiten 10 - 13 vielleicht ein wenig (in einfacheren Worten wie der Prof)
erklären könnte? Ist ne Vorlesung an der Uni Bamberg gewesen:
https://vc.uni-bamberg.de/moodle/pluginfile.php/339143/course/section/156329/Kap%201%2014-10-09.pdf
Was ich bereits weiß bzw. erkannt habe, es handelt sich um einen Algorithmus / Programmablauf und Es gibt 2 Eingaben
nämlich x und y und 2 Ausgaben q und r.
Was ich aber nicht ganz verstehe, es wir ja in der Behauptung auf Seite 10 davon gesprochen, dass es einen Quotienten q gibt? Wo
im Algo wird denn etwas dividiert? → das Gleiche auch bei “Rest bei Division x durch y” → wo wird denn da dividiert?
und die 1. Folie auf Seite 11, ist das ganz unten dann der Beweis oder die niedergeschriebene Logik? Weis jemand velleicht wie die korrekte Aussprache lautet?
oder ist das die Definition bzw. die Signatur des Programms / Algo
(will das nicht alles durcheinander werden, deswegen frag ich lieber nochmal nach 
)
und die letzte Frage wäre: Was genau ist die logische Deduktion, was genau jetzt das Hoare Kalkül und was die Implikation auf der 1. Folie von Seite 12
Tut mir leid, habe auf youtube Vorlesungsvideos gesehen, aber die bringen mich noch mehr durcheinander und wenn ich Prädikatenlogik google, kommen zwar
viele Dinge, aber auch immer nur von Vorlesungen aus Unis oder der TH, aber ich müsste es mal in etwas einfacheren Worten von jemanden hören bzw. lesen,
dann versteh ich so etwas immer leichter…
außerdem ist bei den anderen gegoogled Dingen meisten die Vorlesung oder das Konzept ganz anders wie bei uns und das kostet mich auch immer viel Zeit mir die
ganzen Beiträge und Videos an zu sehen und dann habe ich aber trotzdem nicht so wirklich die Antworten auf meine Fragen…
Ich habe auch Programmiererfahrungen in PHP und C, und bin auch in Mathe eigentlich immer gut gewesen, aber ich wollte es einfach verstehen, bevor am Dienstag jetzt gleich die
nächste Vorlesung + Übung stattfindet… 
1000 Dank vorab
Beste Grüße
1 „Gefällt mir“
Wichtig hier: Der konkrete Algorithmus steht hier eher im hintergrund. Das Hoare-Kalkül wird hier eben anhand dieses Algorithmus beschrieben.
Hier haben wir einen Algorithmus, von dem wir beweisen wollen, dass er Ganzzahlige Division berechnet! D.h. wir haben nur ≤,+,- in unserer Programmiersprache zur Verfügung und jetzt möchten wir ganzzahlige Division nachrüsten. Einfach nur irgendendeinen Algorithmus programmieren und verwenden reicht hier nicht, wir wollen auch noch beweisen, dass der Algorithmus auch tatsächlich dividiert.
Wir wollen division „programmieren“, d.h. wir haben division noch nicht zur Verfügung. Mit hilfe des Hoare-Tripels (untere Folie Seite 11) wird formuliert, dass nach ausführen des Algorithmus q den quotienten darstellt und r den rest der Division darstellt. Die schwarzen kommentare hier sind nur anschaulich zur Hilfe zu sehen. Das q der Quotient ist und r der rest der division ist durch die Nach-Bedingung des Hoare-Tripels mathematisch ausgedrückt als ¬y≤r ∧ x = r + y•q.
Das drückt in FOL (Logik erster Stufe) ungefähr das aus, was umgangssprachlich hinter „Semantik“ steht: wenn x,y,q,r die Bedingung P erfüllen, wir den Algorithmus S anwerfen und danach diese 4 variablen die werte x’,y’,q’,r’ haben, dann gilt nach terminierung des Algorithmus s die Bedingung Q. (Beachte das in der Formel das hintere S, das hinter dem →, eigenltich ein Q sein sollte – nämlich die Nachbedingung)
Allgemein: Deduktion ist ein Synonym für „Herleitung“. D.h. diese Folie beschreibt, wie man in dem Konkreten Beispiel der Division mit rest herleiten kann, dass der Algorithmus S tatsächlich Division mit rest berechnet. Das Hoare-Kalkül ist eine Menge von regeln, mit denen du die gültigkeit von Hoare-Tripeln P{S}Q herleiten kannst. Und wenn du die Korrektheit eines Algorithmus herleitest, dann besteht die Herleitung, nicht nur aus einer Reihe von Hoare-Regeln, sondern auch aus logischen umformungen (logische Deduktion).
Ein beispiel ist direkt am anfang der Herleitung: Die Formel „true“ impliziert nämlich die formel x = x + y • 0. (Die roten pfeile auf der formel sagen, was aus was logisch hergeleitet wird). Im übrigen sind auf den Folien nicht alle Hoare-Regeln direkt in Seite 10-13 genannt, sondern nur die While-Regel (es gibt auch eine für z.B. zuweisungen r ← x).
(Nachdem ich all das geschrieben habe bemerke ich…) Dieser Foliensatz gibt nur einen überblick, was ihr im Semester macht. Und das wäre auch klar, wenn du in der Vorlesung gewesen wärst. Ich tippe ihr die genaue definition kommt im laufe des Semesters, und dann wird das auch alles detailierter erklärt.
Ceterum censeo… gute Vorlesungsfolien sind kein vollwertiges Skript, d.h. daraus kann man entweder nicht ausschließlich lernen, auch nicht wenn je zwei folien auf eine Din-A4-Seite gesetzt werden. Schreibe ein der Vorlesung mit, oder schau dir andere Mitschriften der vorlesungen an, wenn du mal nicht da bist.
1 „Gefällt mir“
und stell solche Fragen in der Vorlesung oder Uebung, dafuer sind die da.
[quote=nbg12:1413043353]Was ich aber nicht ganz verstehe, es wir ja in der Behauptung auf Seite 10 davon gesprochen, dass es einen Quotienten q gibt? Wo
im Algo wird denn etwas dividiert? → das Gleiche auch bei “Rest bei Division x durch y” → wo wird denn da dividiert?[/quote]
da das errnosys noch nicht ganz erklärt hat:
multiplikation ist vielfaches addieren ein- und derselben zahl und division ist die umkehr(funktion), daher sozusagen das gezählte subtrahieren der immer gleichen zahl, bis die nächste subtraktion einen vorzeichenwechsel bedeuten würde
z.b. 5 / 2 = 2
im algorithmus [zähler]
5 - 2 = 3 [1]
3 - 2 = 1 [2]
1 - 2 < 0
→ 5 / 2 = 2 rest 1
hat man noch keine ganzzahldivision zur verfügung, so muss man diesen algorithmus verwenden, wenn man eine braucht
tut mir wirklich leid, dass ich erst jetzt antworte, aber ich wurde so erschlagen von den ersten Semesterwochen, dass ich gar nicht mehr dazu gekommen bin Euch für Eure Beiträge (die mir übrigens sehr geholfen haben)
zu DANKEN!
Beste Grüße