Složitost důkazů a automatické dokazování - NMAG564

• Anglický název: Proof Complexity and Automated Proof Search
• Zajišťuje: Katedra algebry (32-KA)
• Fakulta: Matematicko-fyzikální fakulta
• Platnost: od 2022
• Semestr: letní
• E-Kredity: 3
• Rozsah, examinace: letní s.:2/0, Zk [HT]
• Počet míst: neomezen
• Minimální obsazenost: neomezen
• 4EU+: ne
• Virtuální mobilita / počet míst pro virtuální mobilitu: ne
• Stav předmětu: zrušen
• Jazyk výuky: angličtina
• Způsob výuky: prezenční
• Způsob výuky: prezenční
• Další informace: http://www.karlin.mff.cuni.cz/~krajicek/auto.html
• Garant: prof. RNDr. Jan Krajíček, DrSc.
• Třída: M Mgr. MSTR; M Mgr. MSTR > Volitelné
• Kategorizace předmětu: Matematika > Algebra
• Neslučitelnost : NALG138
• Záměnnost : NALG138
• Je záměnnost pro: NALG138

Anotace

čeština

Poslední úprava: 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.

angličtina

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

čeština

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.

Sylabus

čeština

Poslední úprava: T_KA (14.05.2013)

• Cook-Reckhow důkazové systémy, polynomiální simulace.

• DPLL algoritmus a resoluce.

• Automatizovatelnost důkazového systému, dostupná interpolace, disjunktní NP dvojice.

• Automatizovatelnost a existence jednosměrných funkcí.

• Neautomatizovatelnost Fregeho systému a jeho podsystému konstantní hloubky.

• Automatizovatelnost stromové resoluce a neautomatizovatelnost obecné resoluce.

• Systémy R(k) a zobecněná automatizovatelnost.

• Existence krátkých důkazů pro náhodné 3DNF formule velké hustoty.

angličtina

Poslední úprava: 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.