Logik und Verifikation

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



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



1. Introduction
What is AI?; Logic: From Plato To Zuse; Verification: Verifying reactive systems, Verifying programs
1. Introduction - 2. Sentential Logic (SL) - Übung 1: Sentential Logic
1.3 Verification; 2.1 Motivation; 2.2 Syntax and Semantics
2. Sentential Logic (SL)
2.2 Syntax and Semantics, 2.3 Some Examples, 2.4 Hilbert Calculus
2. Sentential Logic (SL)
2.4 Hilbert Calculus, Resolution Calculus,
3. Verification I: LT properties
3.1 Motivation, 3.2 Basic transition systems, 3.3 Interleaving and handshaking
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
3. Verification I: LT properties
3.5 LT properties in general, 3.6 LTL
4. First-Order Logic: Semantics
4.1 Motivation, 4.2 FOL: Syntax, 4.3 FOL: Models, 4.4 Exampes: LTL and arithmetic
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
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
5. Verification II: Hoare calculus
5.2 Core Programming Language; 5.3 Hoare Logic; 5.4 Proof Calculi: Partial Correctness
5. Verification II: Hoare calculus
5.4 Proof Calculi: Partial Correctness, 5.5 Proof Calculi: Total Correctnes, 5.6 Sound and Completeness
6. From FOL to PROLOG
6. Form FOL to PROLOG: 6.1 Motivation, 6.2 A calculus for FOL, 6.3 Resolution
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
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
7.4 Search Trees and Negation; 7.5 Recursion and Lists; 7.6 Arithmetic; 7.7 Programming; Übung 6 und 7