SubjectsSubjects(version: 996)
Course, academic year 2026/2027
   
Propositional and Predicate Logic - NAIL062
Title: Výroková a predikátová logika
Form of teaching: lecture+practicals
Guaranteed by: Department of Theoretical Computer Science and Mathematical Logic (32-KTIML)
Faculty: Faculty of Mathematics and Physics
Actual: from 2026
Duration in semesters: 1
Semester: winter
E-Credits: 5
Hours per week, examination: winter s.:2/2, C+Ex [HT]
Capacity: unlimited
Maximum number of enrolled students: unlimited
Min. number of students: unlimited
4EU+: no
Virtual mobility / capacity: no
State of the course: taught
Language: Czech, English
Teaching methods: full-time
Additional information: https://jbulin.github.io/teaching/fall/nail062/
Repeated enrollment: 2 / 2 / 2 / 2
Guarantor: doc. Mgr. Petr Gregor, Ph.D.
RNDr. Jakub Bulín, Ph.D.
Teacher(s): RNDr. Jakub Bulín, Ph.D.
doc. Mgr. Petr Gregor, Ph.D.
RNDr. Jan Hric
Mgr. Jakub Mestek
doc. Mgr. Martin Pilát, Ph.D.
RNDr. Jiří Švancara, Ph.D.
Mgr. Marta Vomlelová, Ph.D.
Class: Informatika Bc.
Classification: Informatics > Theoretical Computer Science
Incompatibility : NAIX062
Interchangeability : NAIX062
Is incompatible with: NAIL023, NLTM006, NAIX062
Is interchangeable with: NAIX062, NAIL023
Annotation -
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
Last update: G_I (05.06.2003)
Aim of the course -

To present elements of propositional and predicate logic.

Last update: Gregor Petr, doc. Mgr., Ph.D. (09.10.2017)
Course completion requirements -

The form of study verification is a course credit and an exam. Obtaining the course credit is a necessary condition for taking the exam, except in the case of early exam dates. Course credit is granted by the instructors of the individual tutorial groups on the basis of the point-based evaluation of the credit tests, or additionally a project, homework assignments, participation, etc. Each credit test may be retaken once. The nature of the other assessed components does not allow for a retake.

Last update: Bulín Jakub, RNDr., Ph.D. (25.07.2026)
Literature -
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.
Last update: Bulín Jakub, RNDr., Ph.D. (18.11.2019)
Course assessment methods and requirements for successful completion, grading scheme -

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.

Last update: Gregor Petr, doc. Mgr., Ph.D. (20.09.2022)
Syllabus -

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.

Last update: Gregor Petr, doc. Mgr., Ph.D. (09.10.2017)
 
Charles University | Information system of Charles University | http://www.cuni.cz/UKEN-329.html