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.
Poslední úprava: T_KAM (20.04.2008)
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.
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
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: prof. RNDr. Pavel Pudlák, DrSc. (01.10.2021)
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
Poslední úprava: prof. RNDr. Pavel Pudlák, DrSc. (01.10.2021)
propositional and predicate logics - language and models
resolution and other propositional proof systems
terms and the logic of equality
term unification
term rewriting systems
proof systems for predicate logic
Herbrand's theorem and cut-elimination
resolution and automated theorem proving
the complexity of propositional calculus and general proof systems
