SubjectsSubjects(version: 920)
Course, academic year 2022/2023
   Login via CAS
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
Virtual mobility / capacity: no
State of the course: taught
Language: Czech, English
Teaching methods: full-time
Guarantor: prof. RNDr. Pavel Pudlák, DrSc.
Class: Informatika Mgr. - Diskrétní modely a algoritmy
Classification: Informatics > Discrete Mathematics
Annotation -
Last update: T_KAM (20.04.2008)
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.
Aim of the course -
Last update: prof. RNDr. Pavel Pudlák, DrSc. (01.10.2021)

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.

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

Oral exam.

Literature -
Last update: T_KAM (20.04.2008)

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

Requirements to the exam -
Last update: doc. Mgr. Jan Kynčl, Ph.D. (04.06.2019)

Oral exam.

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

  • 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
Charles University | Information system of Charles University |