Logic in Computer Science - NMAI067
Title: Logika v informatice
Guaranteed by: Department of Applied Mathematics (32-KAM)
Faculty: Faculty of Mathematics and Physics
Actual: from 2021
Semester: winter
E-Credits: 3
Hours per week, examination: winter s.:2/0, Ex [HT]
Capacity: unlimited
Min. number of students: unlimited
4EU+: no
Virtual mobility / capacity: no
State of the course: taught
Language: Czech, English
Teaching methods: full-time
Guarantor: prof. RNDr. Pavel Pudlák, DrSc.
Teacher(s): prof. RNDr. Pavel Pudlák, DrSc.
Class: Informatika Mgr. - Diskrétní modely a algoritmy
Classification: Informatics > Discrete Mathematics
Opinion survey results   Examination dates   WS schedule   Noticeboard   
Annotation -
In this course students will get acquainted with basic concepts of proof theory (proof systems for propositional and predicate logics) and basic results of this theory (Herbrand's theorem, cut-elimination theorem, Craig's interpolation theorem). These results will be studied from the point of view of complexity; we shall present also some lower bounds. Further the course will cover some results on term rewriting and we shall also recall Godel's incompleteness theorems.
Last update: T_KAM (20.04.2008)
Aim of the course -

The aim of the course is to teach students some parts of mathematical logic that are relevant for computer science. These are mainly topics from proof theory that have application in complexity theory, automated theorem proving, and other fields of theoretical computer science.

Last update: Pudlák Pavel, prof. RNDr., DrSc. (01.10.2021)
Course completion requirements -

Oral exam.

Last update: Kynčl Jan, doc. Mgr., Ph.D. (04.06.2019)
Literature -

S. R. Buss, An introduction to proof theory, in: Handbook of Proof Theory, Elsevier 1988.

S.N. Burris, Logic for Mathematics and Computer Science, Prentice Hall, 1998.

C.-L. Chang, R. C.-T. Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1970

J. Krajíček, Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and Its Applications, Vol. 60, Cambridge University Press, 1995.

P. Pudlák, The lengths of proofs, in: Handbook of Proof Theory, Elsevier 1988.

A.S. Troelstra and H. Schwichtenberg, Basic Proof Theory, Cambridge Univ. Press

Last update: T_KAM (20.04.2008)
Requirements to the exam -

Oral exam.

Last update: Kynčl Jan, doc. Mgr., Ph.D. (04.06.2019)
Syllabus -

  • basic concepts, syntax, semantics
  • propositional Resolution system, feasible interpolation, SAT solvers,\dots
  • 3 main formalizations of proofs: Hilbert/Frege style, Gentzen's sequent calculus, Natural Deduction
  • the Cut-elimination Theorem and its applications
  • Herbrand's Theorem
  • bounds on the size of cut-free proofs and Herbrand's disjunction
  • first-order Resolution and automated theorem proving
  • selfreference, Godel's theorems, Rosser's theorem
  • if time permits more
Last update: Pudlák Pavel, prof. RNDr., DrSc. (01.10.2021)