hidden - assigned and confirmed by the Study Dept.
Date of registration:
07.12.2006
Date of assignment:
07.12.2006
Date and time of defence:
10.09.2008 00:00
Date of electronic submission:
10.09.2008
Date of submission of printed version:
10.09.2008
Date of proceeded defence:
10.09.2008
Opponents:
prof. RNDr. Pavel Pudlák, DrSc.
Guidelines
Sestrojit důkazy některých známých tautologií v jednom z algebraických důkazových systémů pro výrokovou logiku.
References
S.Buss, R.Impagliazzo, J.Krajicek, P.Pudlak, A.A.Razborov a J.Sgall, Proof complexity in algebraic systems and bounded depth Frege systems with modular counting, Computational Complexity, 6(3), str.256-298, (1996/97).
S.Cook a R.Reckhow, The relative efficiency of propositional proof systems, J. of Symbolic Logic, 44(1), str.36-50, (1979).
J.Krajicek: Bounded arithmetic, propositional logic, and complexity theory, Cambridge U. Press, (1995).
J.Krajicek, Dehn function and lengths of proofs, Int.J. of Algebra and Computation, 13(5), str.525-542, (2003).
Preliminary scope of work
Obecný pojem výrokového důkazového systému (definován Cookem a Reckhowem) zobecňuje obvyklé výrokové počty. Některé z těchto systémů používají algebru (např. Nullstellensazt). Úkolem práce je sestrojit důkazy konkrétních tautologií v jednom z těchto systémů.
Preliminary scope of work in English
The general notion of a propositional proof system (defined by Cook and Reckhow) generalizes usual propositional calculi. Some of these systems are based on algebra (e.g. Nullstellensatz). The goal of the project is to construct proofs of particular tautologies in one of such systems.