Prednáška se zabývá složitostí automatického dokazování ve výrokové logice z pohledu teorie výpočetní složitosti,
zejména pak tzv. důkazové složitosti. Zakladním problémem je, jak složité je najít důkaz formule v daném
(libovolném) důkazovém systému.
Poslední úprava: T_KA (14.05.2013)
The course is concerned with the complexity of automated proof search in propositional logic from the point of view of
computational complexity theory and, in particular, proof complexity. The basic problem is how complex it is to find a proof of
a formula in a given (arbitrary) proof system.
Literatura -
Poslední úprava: T_KA (14.05.2013)
M.Alekhnovich a A.A.Razborov, Resolution is Not Automatizable Unless W[P] is Tractable, SIAM Journal on Computing, Vol. 38, No 4, (2008), pp.1347-1363.
A.Atserias a M. L. Bonet, On the Automatizability of Resolution and Related Propositional Proof Systems, Information and Computation, 189(2), (2004), pp.182-201.
E.Ben-Sasson a A.Wigderson, Short Proofs are Narrow- Resolution made Simple, Journal of the ACM, 48(2), (2001).
U.Feige a E.Ofek, Easily refutable subformulas of large random 3CNF formulas, Th. of Comp., 3, (2007), pp.25-43.
J.Krajíček, Bounded arithmetic, propositional logic, and complexity theory, Cambridge University Press, (1995).
J.Krajíček a P.Pudlák: Some consequences of cryptographical conjectures for $S^1_2$ and $EF$", Information and Computation, Vol.140(1), (1998), pp.82-94.
P.Pudlák: On reducibility and symmetry of disjoint NP-pairs, Theor.Comput.Science, 295, (2003), pp.323-339.
Poslední úprava: T_KA (14.05.2013)
M.Alekhnovich a A.A.Razborov, Resolution is Not Automatizable Unless W[P] is Tractable, SIAM Journal on Computing, Vol. 38, No 4, (2008), pp.1347-1363.
A.Atserias a M. L. Bonet, On the Automatizability of Resolution and Related Propositional Proof Systems, Information and Computation, 189(2), (2004), pp.182-201.
E.Ben-Sasson a A.Wigderson, Short Proofs are Narrow- Resolution made Simple, Journal of the ACM, 48(2), (2001).
U.Feige a E.Ofek, Easily refutable subformulas of large random 3CNF formulas, Th. of Comp., 3, (2007), pp.25-43.
J.Krajíček, Bounded arithmetic, propositional logic, and complexity theory, Cambridge University Press, (1995).
J.Krajíček a P.Pudlák: Some consequences of cryptographical conjectures for $S^1_2$ and $EF$", Information and Computation, Vol.140(1), (1998), pp.82-94.
P.Pudlák: On reducibility and symmetry of disjoint NP-pairs, Theor.Comput.Science, 295, (2003), pp.323-339.