Toto jsou možné otázky u zkoušky (possible questions at the exam):
Formalizace výrokové logiky. (Formalizations of the propositional calculus.)
Resoluce a Davis-Putnamova procedura.
Tři základní formalizace logiky 1. řádu. (The three basic formalizations of 1st order logic.)
Eliminace řezů v sekvenčním kalkulu. (Cut-elimination in the sequent calculus.)
Věta o interpolaci pro výrokovou logiku a její důkaz. (Craig's Interpolation theorem for the propositional calculus.)
Feasible interpolation for Resolution.
Herbrandova věta a její důkaz z věty o středním sekventu. (Herbrand's theorem and its proof from the mid-sequent theorem.)
Použití H. věty pro automatické dokazováni - resoluce v logice 1. řádu. (Application of H. theorem in automated theorem proving - 1st order resolution).
Godelovy věty a Rosserova věta. (Godel's and Rosser's theorems.)
Lambda calculus as a proof system for intuitionistic propositional logic.
Peano Arithmetic and its weak fragments.
Pokud vám není něco jasné, přijďte na konzultaci! (Come to see me for consultation if anything is unclear.)
The exam will be oral. You will get a question and then you will have 20+ minutes to prepare an answer. During the preparation period you should write down definitions, theorems and sketches of proofs.
Nejdůležitější je (most important is) 1. a slajdy (and slides).
S. Buss, An introduction to proof theory, and First-Order Proof Theory of Arithmetic, the first two chapters in Handbook of Proof Theory, edited by S. Buss, Elsevier North-Holland, 1998, pp 1-78. (download here)
C.L. Chang and R. C.-T. Lee: Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973
P. Hájek, P. Pudlák: Metamathematics of first order arithmetic, Springer-Verlag/ASL Pespectives in Logic, 1998 Kniha je ke stažení přes Project Euclid (can be downloaded using Project Euclid)
C. Smorynski: The incompleteness theorems. Handbook of Mathematical Logic, J. Barwise Editor, 1977.
A.S. Troelstra and H. Schwichtenberg: Basic Proof Theory, Cambridge University Press
10.1.2022