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)
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
Cíl předmětu -
Poslední úprava: T_KTI (26.05.2008)
Naučit základy výrokové a predikátové logiky
Poslední úprava: Mgr. Petr Gregor, Ph.D. (09.10.2017)
To present elements of propositional and predicate logic.
Podmínky zakončení předmětu -
Poslední úprava: Mgr. Petr Gregor, Ph.D. (11.10.2017)
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í průběžný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: Mgr. Petr Gregor, Ph.D. (11.10.2017)
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 point evaluation of tests during the semester, possible homeworks, activity etc. The nature of study verification for the credit excludes the possibility of its repetition.
Požadavky ke zkoušce -
Poslední úprava: Mgr. Petr Gregor, Ph.D. (09.10.2017)
Zkouška se skládá z písemné a ústní části. Písemná část předchází části ústní, její nesplnění znamená, že celá zkouška je hodnocena známkou nevyhověl(a) a ústní částí se již nepokračuje. Nesložení ústní části znamená, že při příštím termínu je nutno opakovat obě části zkoušky, písemnou i ústní. Výsledná známka ze zkoušky se stanoví na základě hodnocení písemné i ústní části.
Písemná část se skládá ze tří příkladů. Vzory písemné části z minulých let jsou k dispozici na stránce k přednášce.
Požadavky u ústní části zkoušky odpovídají sylabu předmětu v rozsahu, který byl prezentován na přednášce.
Poslední úprava: Mgr. Petr Gregor, Ph.D. (09.10.2017)
The exam consists of written and oral parts. The written part precedes the oral part. If the written part is evaluated as unsatisfactory, the exam ends as unsatisfactory without taking the oral part. If the oral part is evaluated as unsatisfactory, the student has to repeat both written and oral parts on the next exam term. Final exam grade is based on evaluation of both written and oral parts.
The written part consist of three problem sets. Examples of the written part from previous years are available on the course webpage.
Demands at oral part correspond to the syllabus of the course in the extend that has been presented on lectures.
Sylabus -
Poslední úprava: Mgr. Petr Gregor, Ph.D. (09.10.2017)
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: Mgr. Petr Gregor, Ph.D. (09.10.2017)
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.
