PředmětyPředměty(verze: 804)
Předmět, akademický rok 2017/2018
   Přihlásit přes CAS
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 2006
Semestr: zimní
E-Kredity: 3
Rozsah, examinace: zimní s.:2/0 Zk [hodiny/týden]
Počet míst: neomezen
Minimální obsazenost: neomezen
Stav předmětu: vyučován
Jazyk výuky: čeština
Způsob výuky: prezenční
Garant: prof. RNDr. Pavel Pudlák, DrSc.
Třída: Informatika Mgr. - Diskrétní modely a algoritmy
Kategorizace předmětu: Informatika > Diskrétní matematika
Anotace -
Poslední úprava: doc. Mgr. Petr Kolman, Ph.D. (10.06.2012)

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.
Cíl předmětu
Poslední úprava: T_KAM (20.04.2008)

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.

Literatura -
Poslední úprava: T_KAM (20.04.2008)

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

Sylabus -
Poslední úprava: T_KAM (20.04.2008)

1. výroková a predikátová logika - jazyk a modely

2. resoluce a další důkazové sytémy pro výrokový počet

3. termy a logika rovnosti

4. unifikace termů

5. přepisovací sytémy

6. důkazové systémy pro predikátovou logiku

7. Herbrandova věta a eliminace řezů

8. resoluce a automatické dokazování

9. složitost výrokového kalkulu a obecné důkazové systémy

10. Peanova aritmetika a její podsystémy

11. Godelova věta

12. lambda-kalkul

 
Univerzita Karlova | Informační systém UK