SubjectsSubjects(version: 845)
Course, academic year 2018/2019
   Login via CAS
Logic in Computer Science - NMAI067
Title in English: Logika v informatice
Guaranteed by: Department of Applied Mathematics (32-KAM)
Faculty: Faculty of Mathematics and Physics
Actual: from 2006
Semester: winter
E-Credits: 3
Hours per week, examination: winter s.:2/0 Ex [hours/week]
Capacity: unlimited
Min. number of students: unlimited
State of the course: taught
Language: Czech
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 - Czech
Last update: T_KAM (20.04.2008)

Vpřednášce se studenti seznámí s partiemi matematické logiky, které mají použití v informatice. Jedná se zejména o oblasti teorie důkazů, které mají uplatnění v teorii složitosti, v automatickém dokazování a dalších oborech teoretické informatiky.

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 - Czech
Last update: prof. RNDr. Pavel Pudlák, DrSc. (24.05.2019)

Formalizace výrokové logiky, resoluce.

Tři základní formalizace logiky 1. řádu.

Eliminace řezů v sekvenčním kalkulu.

Věta o interpolaci pro výrokovou logiku a její důkaz.

Herbrandova věta a její důkaz z věty o středním sekventu.

Použití H. věty pro automatické dokazováni - resoluce v logice 1. řádu.

Godelovy věty a nedefinovatelnost pravdy.

Syllabus -
Last update: T_KAM (20.04.2008)

propositional and predicate logics - language and models

resolution and other propositional proof systems

terms and the logic of equality

term unification

term rewriting systems

proof systems for predicate logic

Herbrand's theorem and cut-elimination

resolution and automated theorem proving

the complexity of propositional calculus and general proof systems

Peano Arithmetic and its subsystems

Godel's theorems

introduction to lambda calculus

 
Charles University | Information system of Charles University | http://www.cuni.cz/UKEN-329.html