Lehrinhalte
syntax and semantics of propositional logic,
functional completeness and normal forms, compactness, complete proof calculi: resolution and a sequent calculus;
\newline
syntax and semantics of first-order logic,
structures and assignments, normal forms, Skolemization, Herbrand theorem, compactness, complete proof calculi: (ground) resolution and a sequent calculus,
Gödel's Completeness Theorem;
undecidability of first-order logic;
\newline
optional: digressions on expressiveness and model checking
Literature
Burris: Logic for Mathematics and Computer Science
\newline
Schöning: Logik für Informatiker
\newline
Boolos, Burgess, Jeffrey: Computability and Logic
\newline
Skript (2 Teile, elektronisch unter www.mathematik.tu-darmstadt.de/otto)
Voraussetzungen
automata, formal languages and decidability
syntax and semantics of propositional logic,
functional completeness and normal forms, compactness, complete proof calculi: resolution and a sequent calculus;
\newline
syntax and semantics of first-order logic,
structures and assignments, normal forms, Skolemization, Herbrand theorem, compactness, complete proof calculi: (ground) resolution and a sequent calculus,
Gödel's Completeness Theorem;
undecidability of first-order logic;
\newline
optional: digressions on expressiveness and model checking
Literature
Burris: Logic for Mathematics and Computer Science
\newline
Schöning: Logik für Informatiker
\newline
Boolos, Burgess, Jeffrey: Computability and Logic
\newline
Skript (2 Teile, elektronisch unter www.mathematik.tu-darmstadt.de/otto)
Voraussetzungen
automata, formal languages and decidability
- Lehrende: Ulrich Kohlenbach
- Lehrende: Pedro Pinto
- Lehrende: Marius Tritschler
Semester: ST 2022