Logik und Verifikation

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

\

Beschreibung

This course is about logic based formal methods and how to use them for verification in computer science.
It rigorously defines the language and semantics of sentential logic (SL) and first-order logic (FOL).
We introduce the notion of a model, and show how hardware and software systems can be modelled within this framework. We also consider
semantic entailment vs. syntactic derivability of formulae and how these two notions are related through correctness and completeness. Completeness is formally proved for SL and extensively discussed for FOL (in the form of refutation completeness).
Both logics are applied to important verification problems: SL and its extension LTL for verifying linear temporal properties in concurrent systems, and
FOL for verifying input/output properties of programs (the Hoare calculus).
We show how the resolution calculus for FOL leads to PROLOG, a programming language based on FOL.
We also show that SL leads to a declarative version of PROLOG: Answer Set Programming (ASP), that can be used to solve problems expressible on the second level of the polynomial hierarchy.
While ASP is not a full-fledged programming language, it can be used for many naturally ocurring problems and it allows to model them in a purely declarative way.

1. Introduction
2. Sentential Logic (SL)
3. Verification I: Reactive Systems
4. First-Order Logic (FOL)
5. Verification II: Hoare Calculus
6. From FOL to PROLOG
7. PROLOG

4.2016

Vorlesungsaufzeichnungen

11.04.201601:33:08683
1. Introduction
What is AI?; Logic: From Plato To Zuse; Verification: Verifying reactive systems, Verifying programs
12.04.201601:36:35811
1. Introduction - 2. Sentential Logic (SL) - Übung 1: Sentential Logic
1.3 Verification; 2.1 Motivation; 2.2 Syntax and Semantics
18.04.201601:25:18515
2. Sentential Logic (SL)
2.2 Syntax and Semantics, 2.3 Some Examples, 2.4 Hilbert Calculus
19.04.201601:28:51742
2. Sentential Logic (SL)
2.4 Hilbert Calculus, Resolution Calculus,
25.04.201601:13:12622
3. Verification I: LT properties
3.1 Motivation, 3.2 Basic transition systems, 3.3 Interleaving and handshaking
02.05.201601:28:42555
3. Verification I: LT properties
3.2 Basic transitions systems, 3.3 Interleaving and handshaking, 3.4 State-space explosions, 3.5 LT properties in gerneral
03.05.201601:36:53648
3. Verification I: LT properties
3.5 LT properties in general, 3.6 LTL
09.05.201601:31:41671
4. First-Order Logic: Semantics
4.1 Motivation, 4.2 FOL: Syntax, 4.3 FOL: Models, 4.4 Exampes: LTL and arithmetic
23.05.201601:20:24479
4. First-Order Logic: Semantics
4.1 Motivation, 4.2 FOL: Syntax, 4.3 FOL: Models, 4.4 Examples: LTL and arithmetic, 4.5 Prenex normal form and clauses
30.05.201601:27:27426
4. First-Order Logic: Semantics; 5. Verification II: Hoare calculus
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
31.05.201601:20:35425
5. Verification II: Hoare calculus
5.2 Core Programming Language; 5.3 Hoare Logic; 5.4 Proof Calculi: Partial Correctness
06.06.201601:06:49460
5. Verification II: Hoare calculus
5.4 Proof Calculi: Partial Correctness, 5.5 Proof Calculi: Total Correctnes, 5.6 Sound and Completeness
13.06.201601:21:03407
6. From FOL to PROLOG
6. Form FOL to PROLOG: 6.1 Motivation, 6.2 A calculus for FOL, 6.3 Resolution
14.06.201601:20:22321
6. Form FOL to PROLOG; 7. PROLOG
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
20.06.201601:32:45247
7. Queries and Matching, PROLOG; Search Trees and Negation
7. 3 Queries and Matching, Einführung PROLOG, Beispiele; 7.4 Search Trees and Negation, Beispiele
27.06.201601:07:52187
7. PROLOG
7.4 Search Trees and Negation; 7.5 Recursion and Lists; 7.6 Arithmetic; 7.7 Programming; Übung 6 und 7