PředmětyPředměty(verze: 908)
Předmět, akademický rok 2022/2023
   Přihlásit přes CAS
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 2015
Semestr: letní
E-Kredity: 3
Rozsah, examinace: letní s.:2/0, Zk [HT]
Počet míst: neomezen
Minimální obsazenost: neomezen
Virtuální mobilita / počet míst: ne
Stav předmětu: nevyučován
Jazyk výuky: angličtina
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
Výsledky anket   Termíny zkoušek   Rozvrh   Nástěnka   
Anotace -
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.
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.

Sylabus -
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.

 
Univerzita Karlova | Informační systém UK