Požadavky ke zkoušce z předmětu Logika v informatice

Toto jsou možné otázky u zkoušky:
  1. Formalizace výrokové logiky, resoluce.
  2. Tři základní formalizace logiky 1. řádu.
  3. Eliminace řezů v sekvenčním kalkulu.
  4. Věta o interpolaci pro výrokovou logiku a její důkaz.
  5. Herbrandova věta a její důkaz z věty o středním sekventu.
  6. Použití H. věty pro automatické dokazováni - resoluce v logice 1. řádu.
  7. Godelovy věty a nedefinovatelnost pravdy.
Pokud vám není něco jasné, přijďte na konzultaci!

Literatura

Nejdůležitější je 1.
  1. S. Buss, An introduction to proof theory, in Handbook of Proof Theory, edited by S. Buss, Elsevier North-Holland, 1998, pp 1-78. pdf
  2. C.L. Chang and R. C.-T. Lee: Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973
  3. 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
  4. C. Smorynski: The incompleteness theorems. Handbook of Mathematical Logic, J. Barwise Editor, 1977.
  5. A.S. Troelstra and H. Schwichtenberg: Basic Proof Theory, Cambridge University Press

13.1.2017