Název:

Matematická logika

Zkratka:MLD
Ak.rok:2012/2013
Semestr:letní
Studijní plán:
ProgramOborRočníkPovinnost
VTI-DR-4DVI4-volitelný
Vyučovací jazyk:čeština
Ukončení:zkouška (kombinovaná)
Výuka:
hod./sempřednáškasem./cvičenílab. cvičenípoč. cvičeníjiná
Rozsah:260000
 zkouškatestycvičenílaboratořeostatní
Body:1000000
Garant:Šlapal Josef, prof. RNDr., CSc., ÚM OADM
Přednášející:Šlapal Josef, prof. RNDr., CSc., ÚM OADM
Fakulta:Fakulta strojního inženýrství VUT
Pracoviště:Ústav matematiky - odbor algebry a diskrétní matematiky FSI VUT
 
Cíle předmětu:
 Cílem předmětu je seznámit studenty se základními metodami uvažování v matematice. Studenti by si měli osvojit obecné principy predikátové logiky a získat tak schopnost přesného matematického uvažování a vyjadřování. Také by se měli naučit pracovat s některými dalšími důležitými formálními teoriemi využívanými v informatice.
Anotace:
V předmětu budou systematicky vyloženy základy výrokové a zejména predikátové logiky. Nejprve budou studenti seznámeni se syntaxí a sémantikou těchto logik, pak budou logiky studovány jako formální teorie s důrazem na problematiku dokazování formulí. Prodiskutovány budou také klasické věty o korektnosti,  úplnosti a kompaktnosti. Po probrání převodu formulí na prenexní tvar budou uvedeny některé vlastnosti a modely teorií 1. řádu. Pozornost bude také věnována nerozhodnutelnosti teorií 1. řádu vyplývající ze známých Gödelových vět o neúplnosti.
Požadované prerekvizitní znalosti a dovednosti:
Předpokládají se znalosti získané v předmětech Diskrétní matematika v bakalářském stupni studia a Matematické struktury v informatice v magisterském stupni studia.
Získané dovednosti, znalosti a kompetence z předmětu:
Studenti se naučí exaktnímu formálnímu myšlení, které jim umožní provádět korektní a efektivní algoritmizaci řešení zadaných problémů. Také získají schopnost ověřovat správnost již vytvořených algoritmizací (verifikace programů).
Dovednosti, znalosti a kompetence obecné:
Studenti se naučí exaktnímu formálnímu myšlení, které jim umožní provádět korektní a efektivní algoritmizaci řešení zadaných problémů. Také získají schopnost ověřovat správnost již vytvořených algoritmizací (verifikace programů).
Osnova přednášek:
  1. Základy teorie množin a kardinální aritmetiky
  2. Základy univeryální algebry 
  3. Jazyk, formule a sémantika výrokové logiky
  4. Formální systém výrokové logiky
  5. Dokazatelnost ve výrokové logice, věta o úplnosti
  6. Jazyk predikátové logiky, termy a formule
  7. Sémantika predikátové logiky
  8. Formální systém predikátové logiky 1. řádu
  9. Dokazatelnost v predikátové logice
  10. Prenexní tvar formulí 
  11. Teorie 1. řádu a jejich modely  
  12. Věta o úplnosti a o kompaktnosti
  13. Nerozhodnutelnost teorií prvního řádu, Gödelovy věty o neúplnosti
Literatura referenční:
  1. E. Mendelson, Introduction to Mathematical Logic, Chapman&Hall, 2001
  2. A. Nerode, R.A. Shore, Logic for Applications, Springer-Verlag 1993
  3. D.M. Gabbay, C.J. Hogger, J.A. Robinson, Handbook of Logic for Artificial Intelligence and Logic Programming, Oxford Univ. Press 1993
  4. G. Metakides, A. Nerode, Principles of logic and logic programming, Elsevier, 1996
  5. Melvin Fitting, First order logic and automated theorem proving, Springer, 1996
  6. Sally Popkorn, First steps in modal logic, Cambridge Univ. Press, 1994
Literatura studijní:
  1. E. Mendelson, Introduction to Mathematical Logic, Chapman&Hall, 2001
  2. A. Nerode, R.A. Shore, Logic for Applications, Springer-Verlag 1993
  3. D.M. Gabbay, C.J. Hogger, J.A. Robinson, Handbook of Logic for Artificial Intellogence and Logic Programming, Oxford Univ. Press 1993
  4. G. Metakides, A. Nerode, Principles of logic and logic programming, Elsevier, 1996
  5. Melvin Fitting, First order logic and automated theorem proving, Springer, 1996
  6. Sally Popkorn, First steps in modal logic, Cambridge Univ. Press, 1994
  7. A. Sochor, Klasická matematická logika, Karolinum, 2001
  8. V. Švejnar, Logika, neúplnost a složitost, Academia, 2002