Video-Server > Vorlesungen > Logik und Verifikation

Logik und Verifikation

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

22:31 Std1.240 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 dem Internet Explorer wird zudem die aktuelle Version des Adobe Flash Players benötigt. Der Internet Explorer wird nur in Version 11 unterstützt. Die Wiedergabe ist mit dem Internet Explorer in Windows 8 oder höher nicht möglich.



Vorlesungen


1. Introduction

Vorlesung Nr. 1

01:33 Std11.04.2016157 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

Vorlesung Nr. 2

01:36 Std12.04.2016124 Aufrufe

Vorlesung starten

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

2. Sentential Logic (SL)

Vorlesung Nr. 3

01:25 Std18.04.201676 Aufrufe

Vorlesung starten

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

2. Sentential Logic (SL)

Vorlesung Nr. 4

01:28 Std19.04.201686 Aufrufe

Vorlesung starten

Inhalt:
2.4 Hilbert Calculus, Resolution Calculus,

3. Verification I: LT properties

Vorlesung Nr. 5

01:13 Std25.04.201669 Aufrufe

Vorlesung starten

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

3. Verification I: LT properties

Vorlesung Nr. 6

01:28 Std02.05.201693 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

Vorlesung Nr. 7

01:36 Std03.05.201697 Aufrufe

Vorlesung starten

Inhalt:
3.5 LT properties in general, 3.6 LTL

4. First-Order Logic: Semantics

Vorlesung Nr. 8

01:31 Std09.05.201695 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

Vorlesung Nr. 9

01:20 Std23.05.201656 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

Vorlesung Nr. 10

01:27 Std30.05.201657 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

Vorlesung Nr. 11

01:20 Std31.05.201665 Aufrufe

Vorlesung starten

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

5. Verification II: Hoare calculus

Vorlesung Nr. 12

01:06 Std06.06.201663 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

Vorlesung Nr. 13

01:21 Std13.06.201657 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

Vorlesung Nr. 14

01:20 Std14.06.201687 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

Vorlesung Nr. 15

01:32 Std20.06.201632 Aufrufe

Vorlesung starten

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

7. PROLOG

Vorlesung Nr. 16

01:07 Std27.06.201626 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 2017