1 - Grundlagen der Logik in der Informatik [ID:6716]
50 von 285 angezeigt

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

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

 

Einbetten
Wordpress FAU Plugin
iFrame
Teilen