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.
Last update: T_KA (14.05.2013)
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.
Literature -
Last update: 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.
Last update: 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.
Syllabus -
Last update: T_KA (14.05.2013)
Cook-Reckhow proof systems,polynomial simulation.
DPLL algoritm and resolution.
Automatizability of a proof system, feasible interpolation, disjoint NP pairs.
Automatizability and the existence of one-way functions.
Non-automatizability of Frege system and of its constant depth subsystems.
Automatizability of tree-like resolution and non-automatizability of general resolution.
Systems R(k) and essential automatizability.
The existence of short proofs of random 3DNF formulas of high density.
