SubjectsSubjects(version: 890)
Course, academic year 2020/2021
Propositional and Predicate Logic - NAIL062
Title: Výroková a predikátová logika
Guaranteed by: Department of Theoretical Computer Science and Mathematical Logic (32-KTIML)
Faculty: Faculty of Mathematics and Physics
Actual: from 2020
Semester: winter
E-Credits: 5
Hours per week, examination: winter s.:2/2 C+Ex [hours/week]
Capacity: unlimited
Min. number of students: unlimited
Virtuální mobilita / počet míst: no
State of the course: taught
Language: Czech, English
Teaching methods: full-time
Additional information:
Guarantor: doc. Mgr. Petr Gregor, Ph.D.
Class: Informatika Bc.
Classification: Informatics > Theoretical Computer Science
Incompatibility : NAIX062
Interchangeability : NAIX062
Is incompatible with: NLTM006, NAIX062
Is interchangeable with: NAIX062
Annotation -
Last update: 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
Aim of the course -
Last update: doc. Mgr. Petr Gregor, Ph.D. (09.10.2017)

To present elements of propositional and predicate logic.

Course completion requirements -
Last update: doc. 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.

Literature -
Last update: RNDr. Jakub Bulín, Ph.D. (18.11.2019)
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.
Requirements to the exam -
Last update: doc. 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.

Syllabus -
Last update: doc. 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.

Charles University | Information system of Charles University |