Subjects

Your browser does not support JavaScript, or its support is disabled. Some features may not be available.

Proof Complexity and the P vs. NP Problem - NMAG536

Title in English:	Důkazová složitost a P vs. NP problém
Guaranteed by:	Department of Algebra (32-KA)
Faculty:	Faculty of Mathematics and Physics
Actual:	from 2018 to 2019
Semester:	summer
E-Credits:	3
Hours per week, examination:	summer s.:2/0 Ex [hours/week]
Capacity:	unlimited
Min. number of students:	unlimited
State of the course:	not taught
Language:	English
Teaching methods:	full-time
Additional information:	http://www1.karlin.mff.cuni.cz/~krajicek/ds11.html

Guarantor:	prof. RNDr. Jan Krajíček, DrSc.
Class:	M Mgr. MSTR M Mgr. MSTR > Povinně volitelné
Classification:	Mathematics > Algebra
Incompatibility :	NALG139
Interchangeability :	NALG139

Opinion survey results Examination dates Schedule Noticeboard

Annotation -

Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (14.05.2019)

The course is concerned with the so called Cook's program which reduces the P vs. NP problem to the task to prove lengths-of-proofs lower bounds for propositional proofs. Even partial advances in the program have various concequences (e.g. for automated theorem proving or in mathematical logic). The course may not be taught every academic year.

Course completion requirements

Last update: prof. RNDr. Jan Krajíček, DrSc. (06.02.2018)

Oral exam: see http://www.karlin.mff.cuni.cz/~krajicek/zk-ds.html.

Literature -

Last update: T_KA (14.05.2013)

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, S.R. Buss ed., Elsevier, 1998, pp.547-637.

Syllabus -

Last update: T_KA (14.05.2013)

The course is concerned with the so called Cook's program which reduces the P vs. NP problem to the

task to prove lengths-of-proofs lower bounds for propositional proofs. Even partial advances in the program

have various concequences (e.g. for automated theorem proving or in mathematical logic).