Video-Server > Vorlesungen > Logik und Verifikation

Logik und Verifikation

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

22:31 Std388 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.201668 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.201674 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.201640 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.201653 Aufrufe

Vorlesung starten

Inhalt:
2.4 Hilbert Calculus, Resolution Calculus,

3. Verification I: LT properties

Vorlesung Nr. 5

01:13 Std25.04.201638 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.201647 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.201618 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.201610 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.20168 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.20169 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.20165 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.20163 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.20165 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.20162 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.20165 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.20163 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