- Видео 13
- Просмотров 341
LogicLab
Германия
Добавлен 30 июл 2014
Welcome to the "LogicLab" channel! Here, I upload videos on topics related to my research.
As a researcher at the Institute of Discrete Mathematics and Geometry at TU Wien, funded by the Austrian Science Fund (FWF), I focus on proof assistants, constructive mathematics (particularly in algebra and analysis), and several other topics, which you can also find on my website.
On this channel, you will find tutorials on proof assistants, recordings of my lectures, and explanations of my publications.
As a researcher at the Institute of Discrete Mathematics and Geometry at TU Wien, funded by the Austrian Science Fund (FWF), I focus on proof assistants, constructive mathematics (particularly in algebra and analysis), and several other topics, which you can also find on my website.
On this channel, you will find tutorials on proof assistants, recordings of my lectures, and explanations of my publications.
Minlog-Kurs 13 - Ex-Falso und Stabilität
Das 13. Video des Minlog-Kurses behandelt die Ex-Falso- und Stabilitätsaxiome. Es zeigt, wie Minlog teilweise automatisch Beweise für diese Axiome erstellen kann, und erläutert die Schritte, um solche Aussagen manuell zu beweisen und abzuspeichern.
Inhaltsübersicht:
00:15 Erklärung von Stab und Efq und den Arten des Falsums
02:04 Ex-falso mit arithmetischem Falsum
03:53 Kommando "proof-of-efq-at"
05:36 Ex-falso Beweis eines induktiv definierten Prädikats
08:55 Nomenklatur eines Ex-falso Beweises
10:02 Stabilitätsaxiom
11:04 Kommando "proof-of-stab-at"
12:15 Stabilitätsbeweis
Quellen:
- Die Minlog-Webseite: www.mathematik.uni-muenchen.de/~logik/minlog/
Dort werden weitere Quellen zur Anwendung von Mi...
Inhaltsübersicht:
00:15 Erklärung von Stab und Efq und den Arten des Falsums
02:04 Ex-falso mit arithmetischem Falsum
03:53 Kommando "proof-of-efq-at"
05:36 Ex-falso Beweis eines induktiv definierten Prädikats
08:55 Nomenklatur eines Ex-falso Beweises
10:02 Stabilitätsaxiom
11:04 Kommando "proof-of-stab-at"
12:15 Stabilitätsbeweis
Quellen:
- Die Minlog-Webseite: www.mathematik.uni-muenchen.de/~logik/minlog/
Dort werden weitere Quellen zur Anwendung von Mi...
Просмотров: 8
Видео
Minlog-Kurs 12 - Wichtige Taktiken zur Beweisführung
Просмотров 307 часов назад
Im zwölften Video des Minlog-Kurses betrachten wir die nützlichen Befehle „assert“ und „cut“, die es ermöglichen, einen Beweis der Formel A in die Beweise von „B impliziert A“ und „B“ aufzuteilen. Anschließend wird eine kurze Einführung in die Beweissuche in Minlog gegeben. Inhaltsübersicht: 00:00 Vorbemerkungen 01:14 Kommando "assert" 03:31 Kommando "cut" 04:49 Automatische Beweissuche in Minl...
Minlog-Kurs 11 - Entscheidbare Gleichheit
Просмотров 3012 часов назад
In dem elften Video des Minlog-Kurses beschäftigen wir uns mit der entscheidbaren Gleichheit, einer zentralen Programmkonstante in Minlog. Die entscheidbare Gleichheit ist eine Funktion, die zwei Terme einer sogenannten finitären Algebra vergleicht und ihnen einen booleschen Wert zuordnet. Zunächst skizzieren wir die Definition dieser Gleichheit und erläutern, wie sie in Minlog implementiert wi...
Minlog-Kurs 10 - Programmkonstanten
Просмотров 716 часов назад
Im zehnten Video des Minlog-Kurses geht es um Programmkonstanten, auch als 'definierte Konstanten' (englisch: 'defined constants') bekannt. Am Beispiel der Verdopplungsfunktion 'double' auf den natürlichen Zahlen zeigen wir, wie Programmkonstanten und ihre Berechnungsregeln eingeführt werden und wie Minlog diese Konstanten sowie deren Berechnungsregeln intern handhabt. Darüber hinaus präsentier...
Minlog-Kurs 09 - Leibniz-Gleichheit
Просмотров 1921 час назад
Das neunte Video des Minlog-Kurses behandelt die Leibniz-Gleichheit, ein induktiv definiertes Prädikat und die stärkste Form der Gleichheit in Minlog. Es wird gezeigt, wie mit der Leibniz-Gleichheit Beweise geführt werden. Außerdem zeigen wir, wie boolesche Terme durch sie als Formeln gesehen verstanden werden. Inhaltsübersicht: 00:00 Leibniz-Gleichheit als induktiv definiertes Prädikat in Minl...
Minlog-Kurs 08 - Totalität
Просмотров 16День назад
In der der Minlog zugrundeliegenden Theorie der berechenbaren Funktionale (TCF) muss nicht jeder Term notwendigerweise total sein. Am Beispiel der natürlichen Zahlen bedeutet dies, dass nicht jeder Term die Form S...S0 hat. Das Totalitätsprädikat für natürliche Zahlen umfasst jedoch genau diese Zahlen. In diesem achten Video des Minlog-Kurses geht es um die Totalität in Minlog. Wir zeigen, wie ...
Minlog-Kurs 07 - Typen und Terme
Просмотров 10День назад
Im siebten Video des Kurses zum Beweisassistenten Minlog liegt der Fokus auf Typen und Terme in Minlog. Gezeigt wird, wie Algebren definiert werden wie beispielsweise die Algebra der natürlichen Zahlen. Zusätzlich werden simultan definierte Algebren betrachtet. Ein weiterer Schwerpunkt ist der Umgang mit Termen. Es wird erläutert, wie Konstruktoren in Terme eingebaut werden und wie Lambda-Abstr...
Minlog-Kurs 06 - Beweise mit induktiv definierten Prädikaten
Просмотров 614 дней назад
Im sechsten Video des Minlog-Kurses zeigen wir, wie man Beweise mit den simultan induktiv definierten Prädikaten 'Even' (gerade) und 'Odd' (ungerade) führt. Wir erklären, wie induktiv definierte Prädikate (IDP) als kleinste Fixpunkte ihrer Einführungsregeln interpretiert werden können. Außerdem geben wir eine erste Einführung in das Konzept der Induktion in Minlog. Inhaltsübersicht: 01:04 Bewei...
Minlog-Kurs 05 - Deklaration induktiv definierter Prädikate
Просмотров 1314 дней назад
In diesem Video ist der erste Teil über allgemeine induktiv definierte Prädikate (IDP) in Minlog. Zunächst werden die bereits bekannten Beispiele wie Konjunktion, Disjunktion und Existenzquantoren behandelt und die verschiedenen Varianten dieser induktiv definierten Prädikate sowie deren rechnerischer Gehalt erklärt. Anschließend wird demonstriert, wie IDP allgemein in Minlog eingegeben werden....
Minlog-Kurs 04 - Konjunktion, Disjunktion
Просмотров 2314 дней назад
Im vierten Teil des Minlog-Kurses geht es um die logischen Operatoren Konjunktion (UND) und Disjunktion (ODER), die in Minlog als induktiv definierte Prädikate realisiert werden. Wir zeigen insbesondere die Einführungs- und Eliminationsregeln dieser Operatoren und geben Befehle an, die in Minlog für Beweise mit Konjunktionen und Disjunktionen verwendet werden. Inhaltsübersicht: 00:00 Vorbemerku...
Minlog-Kurs 03 - Beweise mit Existenzquantoren
Просмотров 1921 день назад
Im dritten Teil des Minlog-Kurses wird gezeigt, wie Beweise mit Existenzquantoren formuliert werden. Der Existenzquantor ist in der zugrunde liegenden Theorie der berechenbaren Funktionale ein Spezialfall eines induktiv definierten Prädikates. Dies wird im Video kurz angesprochen. Die formale Theorie dazu ist in den Quellen, insbesondere im Vorlesungsskript von Prof. Helmut Schwichtenberg, besc...
Minlog-Kurs 02 - Prädikatenlogik
Просмотров 2921 день назад
In diesem zweiten Video zur Arbeit mit dem Beweisassistenten Minlog zeigen wir, wie man Aussagen in der Prädikatenlogik, insbesondere solche mit Allquantoren, formal beweisen kann. Dazu laden wir die Bibliotheksdatei "nat.scm" ein, in der die natürlichen Zahlen eingeführt und zentrale Theoreme darüber bewiesen werden. Inhaltsübersicht: 00:00 Nachtrag zu Teil 1 01:01 Blöcke von Code ausführen 01...
Minlog-Kurs 01 - Metainfos, erster Beweis
Просмотров 13221 день назад
Dieses Video bildet den Auftakt einer mehrteiligen Serie zu Minlog. Es bietet eine Einführung in den Beweisassistenten, der in Scheme geschrieben ist und auf der Theorie der berechenbaren Funktionale (TCF) basiert. Im Video werden grundlegende Informationen zum Kurs sowie zur Bedienung von Minlog vermittelt. In diesem ersten Teil wird ein einfacher Beweis durchgeführt, wobei das Benutzerinterfa...