Dieser Audiobetrag wird von der Universität Erlangen-Nürnberg präsentiert.
Sie finden auch ein Skript auf der Veranstaltungswelle.
Ab diesem Semester ist aufgegeben dieses Skript inoffiziell zu nennen,
also ich ich editiere da schon so lange selber daranrum, nachdem am Anfang mal
Studierende das geschrieben hatten, dass ich mich nicht mehr wirklich davon
distanzieren kann. Das Skript ist aber, steht auch ausdrücklich dran, während des Semesters immer
vorläufig. Also es kann sich, insbesondere am Umfang des Materials, können sich da Änderungen
ergeben. Insbesondere gibt es also keine Garantie, dass nicht auch noch was anderes dran kommt,
als das, was da jetzt drin steht. Das mit der Aufnahme, das ist immer so ein bisschen
zweischneidig. Das gestattet Ihnen, wenn Sie mal nicht können oder krank waren oder einen
Verkehrsunfall hatten oder sonst was unangenehmes und tragisches, dass Sie dann hinterher sich
das Material nochmal angucken können. Gelegentlich stellt man fest, dass also das Vorhandensein
dieser Aufnahme sehr auf den Besuch der Veranstaltung im physischen Sinne drückt. Und die Effekte
davon auf so objektiv messbare Parameter wie insbesondere Bestehensquote der Klausur ist
nicht positiv. Also ich kann Ihnen nur dringend raten, gucken Sie sich das meinetwegen hinterher
an, wenn Sie selber hier waren oder wenn Sie nun absolut nicht konnten, aber nehmen Sie
das mit den Videoaufnahmen nicht zum Anlass, jetzt Ihre physische Anwesenheit hier ganz
aufzugeben. Es ist einfach messbar was anderes, ob man im Saal sitzt und das vor allem, das
das nächste selber mitschreibt, als wenn man es nur hinterher am Bildschirm konsumiert.
Das ist einfach nicht dasselbe. Das bringt mich also zum nächsten Punkt. Es gibt eben
dieses Skript. Im Prinzip haben Sie das alles schriftlich da und wenn ich was ändere, führe
ich das auch nach. Aber nochmal ganz dringende Empfehlung, schreiben Sie hier mit und nehmen
Sie das auch so wichtig, dass Sie mich bremsen, wenn Sie feststellen, dass Sie nicht mitkommen.
Also ich beabsichtige hier nur so schnell zu schreiben, dass das mitgeschrieben werden
kann und wenn das jemand nicht hinkriegt, dann bitte sofort den Arm hoch. Ich mache dann
langsamer und ich warte bis das der letzte abgeschrieben hat. Ich bin auch ein fauler
Mensch, ich bin immer froh, wenn ich weniger anschreiben muss.
Dagegen, also es gibt zwar das jetzt die Materialfrage, also es gibt das Skript, es gibt die Aufnahme,
dagegen nicht geben tut es eben Veranstaltungsfolien. Folien werden hier nicht verwendet, ich mache
alles an der Tafel. Es gibt eine einzige Ausnahme, wir verwenden in einigen Aufgaben ein interaktives
Beweiserwerkzeug, das nennt sich COQ, entwickelt von Franzosen, ja was soll man da sagen. Gut,
also jetzt lassen wir mal die völkerfeindlichen Sprüche hier beiseite. Das ist also auch
etwas, was ich für Sie sehr empfiehlt, also erstens hilft es Ihnen beim Lösen der Übungsaufgaben
und zweitens hilft es beim Verständnis des Materials insofern weiter, als dieses System
keine Fehler zulässt. Sie können da Beweise führen in diesem Tool und das führe ich Ihnen
gelegentlich hier ganz grob vor, deswegen sage ich das, das ist die eine Gelegenheit, wo
dann doch mal der Beamer verwendet wird und das Tool lässt also wirklich nur korrekte
Schlüsse zu. Sie konstruieren da formale Beweise und werden sie auf Papier irgendwie
sagen, das stimmt jetzt schon, macht also der automatische Beweiser das nicht mit.
Das ist also in dem Sinne für Sie unheimlich wichtig. Ich sage das deswegen, weil dieses
interaktive Beweiswerkzeug offensichtlich nicht klausurrelevant ist. Wir können es
nicht hier durchziehen, also dafür müsste man alles auf elektronische Klausuren umstellen.
Also es ist nicht sinnvoll für uns jetzt während der Klausur das Erstellen von Beweisern am
Rechner zu verlangen. Aber was wir durchaus tun ist, in der Klausur formale Beweise verlangen
und da hilft es eben sehr, wenn Sie in der Lage sind diese formalen Beweise am Rechner
zu konstruieren, dann machen Sie eben auch auf Papier keine Fehler, wenn Sie das tun.
Das ist ein frei verfügbares Werkzeug, das ist schnell zu installieren, also insbesondere
wenn Sie Linux verwenden, dann ist das glaube ich einfach als Debian-Paket einspielbar.
Das heißt, es sollte hoffentlich von der Verwendung her keine Schwierigkeiten geben,
oder zumindest von der Softwaretechnischen Verwendung. Gut, das ist jetzt glaube ich
Presenters
Zugänglich über
Offener Zugang
Dauer
00:38:51 Min
Aufnahmedatum
2016-10-17
Hochgeladen am
2016-10-18 10:48:14
Sprache
de-DE
Aussagenlogik:
-
Syntax und Semantik
-
Automatisches Schließen: Resolution
-
Formale Deduktion: Korrektheit, Vollständigkeit
Prädikatenlogik erster Stufe:
-
Syntax und Semantik
-
Automatisches Schließen: Unifikation, Resolution
-
Quantorenelimination
-
Anwendung automatischer Beweiser
-
Formale Deduktion: Korrektheit, Vollständigkeit