Video-Server > Vorlesungen > Logik und Verifikation

Logik und Verifikation

von Prof. Dr. rer. nat. Jürgen Dix

22:31 Std3.287 Aufrufe15.04.2016
Kamera Anja Michaela Kaiser

Hinweise zum Player

Um die Aufzeichnungen auf dieser Webseite wiedergeben zu können, muss Javascript aktiviert sein. Zur Wiedergabe mit Apple iOS Geräten muss im Safari Browser nach Aufruf des Players die Desktop Seite angefordert werden. Der Internet Explorer wird nur in Version 11 in Windows 8 oder höher unterstützt.



Vorlesungen


1. Introduction

01:33 Std11.04.2016392 Aufrufe

Vorlesung starten

Inhalt:
What is AI?; Logic: From Plato To Zuse; Verification: Verifying reactive systems, Verifying programs

1. Introduction - 2. Sentential Logic (SL) - Übung 1: Sentential Logic

01:36 Std12.04.2016353 Aufrufe

Vorlesung starten

Inhalt:
1.3 Verification; 2.1 Motivation; 2.2 Syntax and Semantics

2. Sentential Logic (SL)

01:25 Std18.04.2016245 Aufrufe

Vorlesung starten

Inhalt:
2.2 Syntax and Semantics, 2.3 Some Examples, 2.4 Hilbert Calculus

2. Sentential Logic (SL)

01:28 Std19.04.2016307 Aufrufe

Vorlesung starten

Inhalt:
2.4 Hilbert Calculus, Resolution Calculus,

3. Verification I: LT properties

01:13 Std25.04.2016223 Aufrufe

Vorlesung starten

Inhalt:
3.1 Motivation, 3.2 Basic transition systems, 3.3 Interleaving and handshaking

3. Verification I: LT properties

01:28 Std02.05.2016234 Aufrufe

Vorlesung starten

Inhalt:
3.2 Basic transitions systems, 3.3 Interleaving and handshaking, 3.4 State-space explosions, 3.5 LT properties in gerneral

3. Verification I: LT properties

01:36 Std03.05.2016203 Aufrufe

Vorlesung starten

Inhalt:
3.5 LT properties in general, 3.6 LTL

4. First-Order Logic: Semantics

01:31 Std09.05.2016220 Aufrufe

Vorlesung starten

Inhalt:
4.1 Motivation, 4.2 FOL: Syntax, 4.3 FOL: Models, 4.4 Exampes: LTL and arithmetic

4. First-Order Logic: Semantics

01:20 Std23.05.2016142 Aufrufe

Vorlesung starten

Inhalt:
4.1 Motivation, 4.2 FOL: Syntax, 4.3 FOL: Models, 4.4 Examples: LTL and arithmetic, 4.5 Prenex normal form and clauses

4. First-Order Logic: Semantics; 5. Verification II: Hoare calculus

01:27 Std30.05.2016132 Aufrufe

Vorlesung starten

Inhalt:
4. First-Order Logic: Semantics: 4.5 Prenex normal form and clauses; 4.6 Sit-Calculus; 4.7 The Blocksworld; 4.8 Higher order logic. 5. Verification II: Hoare calculus: 5.1 Motivation; 5.2 Core Programming Language

5. Verification II: Hoare calculus

01:20 Std31.05.2016155 Aufrufe

Vorlesung starten

Inhalt:
5.2 Core Programming Language; 5.3 Hoare Logic; 5.4 Proof Calculi: Partial Correctness

5. Verification II: Hoare calculus

01:06 Std06.06.2016154 Aufrufe

Vorlesung starten

Inhalt:
5.4 Proof Calculi: Partial Correctness, 5.5 Proof Calculi: Total Correctnes, 5.6 Sound and Completeness

6. From FOL to PROLOG

01:21 Std13.06.2016154 Aufrufe

Vorlesung starten

Inhalt:
6. Form FOL to PROLOG: 6.1 Motivation, 6.2 A calculus for FOL, 6.3 Resolution

6. Form FOL to PROLOG; 7. PROLOG

01:20 Std14.06.2016162 Aufrufe

Vorlesung starten

Inhalt:
6. Form FOL to PROLOG: 6.4 Herbrand, 6.5 Variants of resolution, 6.6 SLD resolution; 7. PROLOG: 7.1 Motivation, 7.2 Syntax

7. Queries and Matching, PROLOG; Search Trees and Negation

01:32 Std20.06.2016106 Aufrufe

Vorlesung starten

Inhalt:
7. 3 Queries and Matching, Einführung PROLOG, Beispiele; 7.4 Search Trees and Negation, Beispiele

7. PROLOG

01:07 Std27.06.2016105 Aufrufe

Vorlesung starten

Inhalt:
7.4 Search Trees and Negation; 7.5 Recursion and Lists; 7.6 Arithmetic; 7.7 Programming; Übung 6 und 7


Impressum · Kontakt© TU Clausthal 2018