Metody odhadů složitosti důkazů ve výrokové logice

• Název práce v češtině: Metody odhadů složitosti důkazů ve výrokové logice
• Název v anglickém jazyce: Methods of proving lower bounds in propositional logic
• Klíčová slova: Rezoluce, důkazová složitost, aproximační metoda, Broken Mosquito Screens
• Klíčová slova anglicky: Resolution, proof complexity, approximation method, Broken Mosquito Screens
• Akademický rok vypsání: 2011/2012
• Typ práce: diplomová práce
• Jazyk práce: čeština
• Ústav: Katedra algebry (32-KA)
• Vedoucí / školitel: prof. RNDr. Pavel Pudlák, DrSc.
• Řešitel: skrytý - zadáno a potvrzeno stud. odd.
• Datum přihlášení: 27.10.2011
• Datum zadání: 01.11.2011
• Datum potvrzení stud. oddělením: 02.12.2011
• Datum a čas obhajoby: 13.09.2013 00:00
• Datum odevzdání elektronické podoby: 01.08.2013
• Datum odevzdání tištěné podoby: 02.08.2013
• Datum proběhlé obhajoby: 13.09.2013
• Oponenti: prof. RNDr. Jan Krajíček, DrSc.

Zásady pro vypracování

Cílem práce je zkoumat použití tzv. aproximační metody v důkazové složitosti. Aproximační metodou Razborov dokázal dolní odhady na složitost explicitních funkcí počítaných monotonními obvody. Tento výsledek se dá použít k důkazu dolního odhadu na složitost důkazů ve výrokové resoluci tak, že se pomocí Krajíčkovy efektivní interpolace problém odhadů na složitost důakzů redukuje na odhady složitosti monotonních obvodů. V principu je možné dokázat tento výsledek bez explicitního použití effektivní interpolace. Takový důkaz by mohl naznačit jak aplikovat interpolační metodu i na další důkazové systémy.

Seznam odborné literatury

P. Pudlak: Lower bounds for resolution and cutting planes proofs and monotone computations, J. of Symb. Logic 62(3), 1997, pp.981-998.

C. Berg: On Oracles and Circuits-Topics in Computational Complexity, Doctoral Dissertation, Royal Institute of Technology, 1997.

J. Krajíček: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic, J. of Symbolic Logic, 62(2), (1997), pp.457-486.