|
|
|
||
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)
|
|
||
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)
|
|
||
Ústní zkouška. Poslední úprava: Kynčl Jan, doc. Mgr., Ph.D. (04.06.2019)
|
|
||
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)
|
|
||
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)
|
|
||
viz anglická verze Poslední úprava: Pudlák Pavel, prof. RNDr., DrSc. (01.10.2021)
|