Výroková a predikátová logika - NAIL062

• Anglický název: Propositional and Predicate Logic
• Zajišťuje: Katedra teoretické informatiky a matematické logiky (32-KTIML)
• Fakulta: Matematicko-fyzikální fakulta
• Platnost: od 2023
• Semestr: zimní
• E-Kredity: 5
• Rozsah, examinace: zimní s.:2/2, Z+Zk [HT]
• Počet míst: neomezen
• Minimální obsazenost: neomezen
• 4EU+: ne
• Virtuální mobilita / počet míst pro virtuální mobilitu: ne
• Stav předmětu: vyučován
• Jazyk výuky: čeština, angličtina
• Způsob výuky: prezenční
• Způsob výuky: prezenční
• Další informace: https://jbulin.github.io/teaching/fall/nail062/
• Garant: doc. Mgr. Petr Gregor, Ph.D.; RNDr. Jakub Bulín, Ph.D.
• Vyučující: Mgr. Martin Blicha, Ph.D.; RNDr. Jakub Bulín, Ph.D.; doc. Mgr. Petr Gregor, Ph.D.; RNDr. Jan Hric; Mgr. Kristýna Pantůčková; doc. Mgr. Martin Pilát, Ph.D.; RNDr. Jiří Švancara, Ph.D.; Mgr. Marta Vomlelová, Ph.D.
• Třída: Informatika Bc.
• Kategorizace předmětu: Informatika > Teoretická informatika
• Neslučitelnost : NAIX062
• Záměnnost : NAIX062
• Je neslučitelnost pro: NAIL023, NLTM006, NAIX062
• Je záměnnost pro: NAIX062, NAIL023

Anotace

čeština

Výroková logika, normální tvary formulí, predikátová logika, věty o úplnosti výrokové a predikátové logiky, prenexní tvary formulí, modely teorií 1. řádu. Meze formální metody, Gödelovy věty.

Poslední úprava: G_I (05.06.2003)

angličtina

Propositional logic, normal forms of propositional formulas, predicate logic of first order, prenex forms of formulas, completness theorems for propositional and predicate logic, models of first-order theories. The limits of formal method, Goedel's theorems

Poslední úprava: G_I (05.06.2003)

Cíl předmětu

čeština

Naučit základy výrokové a predikátové logiky

Poslední úprava: T_KTI (26.05.2008)

angličtina

To present elements of propositional and predicate logic.

Poslední úprava: Gregor Petr, doc. Mgr., Ph.D. (09.10.2017)

Podmínky zakončení předmětu

čeština

Formou kontroly studia předmětu je zápočet a zkouška. Získání zápočtu je nutnou podmínkou pro absolvování zkoušky s výjimkou předtermínů. Zápočet udělují vyučující na jednotlivých cvičeních na základě bodového hodnocení zápočtových testů, případných domácích úloh, aktivity apod. Povaha kontroly na zápočet vylučuje možnost jejího opakování.

Poslední úprava: Gregor Petr, doc. Mgr., Ph.D. (20.09.2022)

angličtina

The form of study verification is a credit and an exam. Obtaining credit first is a necessary condition for taking an exam, with the exception of early exam terms. The credit is granted by teachers leading the tutorials based on evaluation of tests during the semester, possibly homework assignments, in-class activities, etc. The nature of study verification for the credit excludes the possibility of its repetition.

Poslední úprava: Gregor Petr, doc. Mgr., Ph.D. (20.09.2022)

Literatura

čeština

A. Nerode, R. A. Shore, Logic for Applications, Springer, 2. vydání, 1997.
P. Pudlák, Logical Foundations of Mathematics and Computational Complexity - A Gentle Introduction, Springer, 2013.
V. Švejdar, Logika, neúplnost, složitost a nutnost, Academia, Praha, 2002.
A. Sochor, Klasická matematická logika, Univerzita Karlova v Praze - Karolinum, 2001.
W. Hodges, Shorter Model Theory, Cambridge University Press, 1997.
W. Rautenberg, A concise introduction to mathematical logic, Springer, 2009.

J. Mlček, Výroková a predikátová logika, el. skripta, 2012.
P. Štěpánek, Meze formální metody, el. skripta, 2000.

Poslední úprava: Bulín Jakub, RNDr., Ph.D. (18.11.2019)

angličtina

A. Nerode, R. A. Shore, Logic for Applications, Springer, 2. vydání, 1997.
P. Pudlák, Logical Foundations of Mathematics and Computational Complexity - A Gentle Introduction, Springer, 2013.
V. Švejdar, Logic: Incompleteness, Complexity, and Necessity, Academia, Praha, 2002.
W. Hodges, Shorter Model Theory, Cambridge University Press, 1997.
W. Rautenberg, A concise introduction to mathematical logic, Springer, 2009.

Literature in Czech only:

A. Sochor, Klasická matematická logika, Univerzita Karlova v Praze - Karolinum, 2001.
J. Mlček, Výroková a predikátová logika, el. skripta, 2012.
P. Štěpánek, Meze formální metody, el. skripta, 2000.

Poslední úprava: Bulín Jakub, RNDr., Ph.D. (18.11.2019)

Požadavky ke zkoušce

čeština

Zkouška je ústní s písemnou přípravou. Požadavky u zkoušky odpovídají sylabu předmětu v rozsahu, který byl pokryt na přednášce.

Poslední úprava: Gregor Petr, doc. Mgr., Ph.D. (20.09.2022)

angličtina

The exam is oral with written preparation. Requirements for the exam correspond to the syllabus of the course in the extent that has been covered in the lecture.

Poslední úprava: Gregor Petr, doc. Mgr., Ph.D. (20.09.2022)

Sylabus

čeština

Výroková logika: základní syntax a sémantika, normální tvary formulí, problém splnitelnosti. Tablo metoda a rezoluce ve výrokové logice. Věta o úplnosti výrokové logiky.

Predikátová logika: základní syntax a sémantika, prenexní tvary formulí, vlastnosti a modely teorií 1. řádu. Tablo metoda a rezoluce v predikátové logice. Skolemova věta, Herbrandova věta. Věta o úplnosti predikátové logiky, kompaktnost.

Kompletnost a její kritéria, rozhodnutelnost. Meze formální metody, Gödelovy věty.

Poslední úprava: Gregor Petr, doc. Mgr., Ph.D. (09.10.2017)

angličtina

Propositional logic: elementary syntax and semantics, normal forms of propositional formulas, problem of satisfiability. Tableau method and resolution in propositional logic. Completeness theorem for propositional logic.

Predicate (first-order) logic: elementary syntax and semantics, prenex normal form of formulas, properties and models of first-order theories. Tableau method and resolution for predicate logic. Skolem's theorem, Herbrand's theorem. Completeness theorem for predicate logic, compactness.

Criteria for completeness, decidability. Limits of formal methods, Goedel's theorems.

Poslední úprava: Gregor Petr, doc. Mgr., Ph.D. (09.10.2017)