Video-Server > Vorlesungen > Logik und Verifikation

Logik und Verifikation

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

22:31 Std2.819 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.2016318 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.2016270 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.2016178 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.2016201 Aufrufe

Vorlesung starten

Inhalt:
2.4 Hilbert Calculus, Resolution Calculus,

3. Verification I: LT properties

Vorlesung Nr. 5

01:13 Std25.04.2016173 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.2016193 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.2016182 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.2016205 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.2016141 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.2016131 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.2016154 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.2016153 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.2016153 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.2016160 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.2016104 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.2016103 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