Logika v informatice - NMAI067

• Anglický název: Logic in Computer Science
• Zajišťuje: Katedra aplikované matematiky (32-KAM)
• Fakulta: Matematicko-fyzikální fakulta
• Platnost: od 2021
• Semestr: zimní
• E-Kredity: 3
• Rozsah, examinace: zimní s.:2/0, Zk [HT]
• Počet míst: neomezen
• Minimální obsazenost: neomezen
• 4EU+: ne
• Virtuální mobilita / počet míst pro virtuální mobilitu: ne
• Stav předmětu: vyučován
• Jazyk výuky: čeština, angličtina
• Způsob výuky: prezenční
• Garant: prof. RNDr. Pavel Pudlák, DrSc.
• Vyučující: prof. RNDr. Pavel Pudlák, DrSc.
• Třída: Informatika Mgr. - Diskrétní modely a algoritmy
• Kategorizace předmětu: Informatika > Diskrétní matematika

Anotace

čeština

V přednášce se studenti seznámí se základními pojmy z teorie důkazů (důkazovými systémy pro výrokovou a predikátovou logiku) a základními výsledky této teorie (Herbrandova věta, věta o eliminaci řezů, Craigova věta o interpolaci). Tyto výsledky budou studovány z hlediska složitosti; ukážeme i některé dolní odhady na složitost důkazů. Dále se přednáška zabývá také přepisováním termů (v případě dostatku času, lambda kalkulem) a připomeneme si i Godelovy věty o neúplnosti.

Poslední úprava: Kolman Petr, doc. Mgr., Ph.D. (10.06.2012)

angličtina

In this course students will get acquainted with basic concepts of proof theory (proof systems for propositional and predicate logics) and basic results of this theory (Herbrand's theorem, cut-elimination theorem, Craig's interpolation theorem). These results will be studied from the point of view of complexity; we shall present also some lower bounds. Further the course will cover some results on term rewriting and we shall also recall Godel's incompleteness theorems.

Poslední úprava: T_KAM (20.04.2008)

Cíl předmětu

čeština

Vpřednášce se studenti seznámí s partiemi matematické logiky, které mají použití v informatice. Jedná se zejména o oblasti teorie důkazů, které mají uplatnění v teorii složitosti, v automatickém dokazování a dalších oborech teoretické informatiky.

Poslední úprava: T_KAM (20.04.2008)

angličtina

The aim of the course is to teach students some parts of mathematical logic that are relevant for computer science. These are mainly topics from proof theory that have application in complexity theory, automated theorem proving, and other fields of theoretical computer science.

Poslední úprava: Pudlák Pavel, prof. RNDr., DrSc. (01.10.2021)

Podmínky zakončení předmětu

čeština

Ústní zkouška.

Poslední úprava: Kynčl Jan, doc. Mgr., Ph.D. (04.06.2019)

angličtina

Oral exam.

Poslední úprava: Kynčl Jan, doc. Mgr., Ph.D. (04.06.2019)

Literatura

čeština

S. R. Buss, An introduction to proof theory, in: Handbook of Proof Theory, Elsevier 1988.

S.N. Burris, Logic for Mathematics and Computer Science, Prentice Hall, 1998.

C.-L. Chang, R. C.-T. Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1970

J. Krajíček, Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and Its Applications, Vol. 60, Cambridge University Press, 1995.

P. Pudlák, The lengths of proofs, in: Handbook of Proof Theory, Elsevier 1988.

A.S. Troelstra and H. Schwichtenberg, Basic Proof Theory, Cambridge Univ. Press

Poslední úprava: T_KAM (20.04.2008)

Požadavky ke zkoušce

čeština

Formalizace výrokové logiky, resoluce.

Tři základní formalizace logiky 1. řádu.

Eliminace řezů v sekvenčním kalkulu.

Věta o interpolaci pro výrokovou logiku a její důkaz.

Herbrandova věta a její důkaz z věty o středním sekventu.

Použití H. věty pro automatické dokazováni - resoluce v logice 1. řádu.

Godelovy věty a nedefinovatelnost pravdy.

Ústní zkouška.

Poslední úprava: Kynčl Jan, doc. Mgr., Ph.D. (04.06.2019)

angličtina

Oral exam.

Poslední úprava: Kynčl Jan, doc. Mgr., Ph.D. (04.06.2019)

Sylabus

čeština

viz anglická verze

Poslední úprava: Pudlák Pavel, prof. RNDr., DrSc. (01.10.2021)

angličtina

• basic concepts, syntax, semantics

• propositional Resolution system, feasible interpolation, SAT solvers,\dots

• 3 main formalizations of proofs: Hilbert/Frege style, Gentzen's sequent calculus, Natural Deduction

• the Cut-elimination Theorem and its applications

• Herbrand's Theorem

• bounds on the size of cut-free proofs and Herbrand's disjunction

• first-order Resolution and automated theorem proving

• selfreference, Godel's theorems, Rosser's theorem

• if time permits more

Poslední úprava: Pudlák Pavel, prof. RNDr., DrSc. (01.10.2021)