Kooperativer Bibliotheksverbund

UID:

Format: 1 Online-Ressource (xvi, 247 pages) , digital, PDF file(s).

ISBN: 9781139107211

Series Statement: London Mathematical Society lecture note series 382

Content: This book introduces a new approach to building models of bounded arithmetic, with techniques drawn from recent results in computational complexity. Propositional proof systems and bounded arithmetics are closely related. In particular, proving lower bounds on the lengths of proofs in propositional proof systems is equivalent to constructing certain extensions of models of bounded arithmetic. This offers a clean and coherent framework for thinking about lower bounds for proof lengths, and it has proved quite successful in the past. This book outlines a brand new method for constructing models of bounded arithmetic, thus for proving independence results and establishing lower bounds for proof lengths. The models are built from random variables defined on a sample space which is a non-standard finite set and sampled by functions of some restricted computational complexity. It will appeal to anyone interested in logical approaches to fundamental problems in complexity theory.

Note: Title from publisher's bibliographic system (viewed on 05 Oct 2015) , 12.1. Witnessing AX〉 xEY〉 x & Sigma;1,b0-formulas -- 12.2. Preservation of true s & Pi;l, b 1-sentences -- 12.3. Circuit lower bound for parity -- pt. IV AC0(2) WORLD -- 13. Theory Q2V01 -- 13.1. Q2 quantifier and theory Q2V01 -- 13.2. Interpreting Q2 in structures -- 14. Algebraic model -- 14.1. Family Falg -- 14.2. Family Galg -- 14.3. Open comprehension and open induction -- 15. Quantifier elimination and the interpretation of Q2 -- 15.1. Skolemization and the Razborov-Smolensky method -- 15.2. Interpretation of Q2 in front of an open formula -- 15.3. Elimination of quantifiers and the interpretation of the Q2 quantifier -- 15.4. Comprehension and induction for Q2 & Sigma;1,b0-formulas -- 16. Witnessing and independence in Q2V01 -- 16.1. Witnessing AX〉 xEY〉 xAZ〉 x & Sigma;1,b0-formulas -- 16.2. Preservation of true ss & Pi;l, b 1-sentences -- pt. V TOWARDS PROOF COMPLEXITY -- 17. Propositional proof systems -- 17.1. Frege and Extended Frege systems. , 17.2. Language with connective and constant-depth Frege systems -- 18. An approach to lengths-of-proofs lower bounds -- 18.1. Formalization of the provability predicate -- 18.2. Reflection principles -- 18.3. Three conditions for a lower bound -- 19. PHP principle -- 19.1. First-order and propositional formulations of PHP -- 19.2. Three conditions for Fd and Fd lower bounds for PHP -- pt. VI PROOF COMPLEXITY OF FD AND FD -- 20. A shallow PHP model -- 20.1. Sample space & Omega;0PHP and PHP-trees -- 20.2. Structure K(F0PHP, G0PHP) and open comprehension and open induction -- 20.3. The failure of PHP in K(F0PHP, G0PHP) -- 21. Model K(FPHP, GPHP) of V01 -- 21.1. The PHP switching lemma -- 21.2. Structure K(FPHP, GPHP) -- 21.3. Open comprehension, open induction and failure of PHP -- 21.4. Bounded quantifier elimination -- 21.5. PHP lower bound for Fd: a summary -- 22. Algebraic PHP model? -- 22.1. Algebraic formulation of PHP and relevant rings -- 22.2. Nullstellensatz proof system NS and designs. , 22.3. A reduction of Fd to NS with extension polynomials -- 22.4. A reduction of polynomial calculus PC to NS -- 22.5. The necessity of partially defined random variables -- pt. VII POLYNOMIAL-TIME AND HIGHER WORLDS -- 23. Relevant theories -- 23.1. Theories PV and ThA(LPV) -- 23.2. Theories S12, T12 and BT -- 23.3. Theories U11 and V11 -- 24. Witnessing and conditional independence results -- 24.1. Independence for S12 -- 24.2. S12 versus T12 -- 24.3. PV versus S12 -- 24.4. Transfer principles -- 25. Pseudorandom sets and a Lowenheim-Skolem phenomenon -- 26. Sampling with oracles -- 26.1. Structures K (Foracle) and K (Foracle, Goracle) -- 26.2. An interpretation of random oracle results -- pt. VIII PROOF COMPLEXITY OF EF AND BEYOND -- 27. Fundamental problems in proof complexity -- 28. Theories for EF and stronger proof systems -- 28.1. First-order context for EF: PV and S12 -- 28.2. Second-order context for EF: VPV and V11 -- 28.3. Stronger proof systems -- 29. Proof complexity generators: definitions and facts. , 29.1. & tau;-formulas and their hardness -- 29.2. The truth-table function -- 29.3. Iterability and the completeness of tts, k -- 29.4. The Nisan-Wigderson generator -- 29.5. Gadget generators -- 29.6. Optimal automatizer for the & tau;-formulas -- 30. Proof complexity generators: conjectures -- 30.1. On provability of circuit lower bounds -- 30.2. Razborov's conjecture on the NW generator and EF -- 30.3. A possibly hard gadget -- 30.4. Rudich's demi-bit conjecture -- 31. The local witness model -- 31.1. The local witness model K(Fb) -- 31.2. Regions of undefinability -- 31.3. Properties of the local model K(Fb) -- 31.4. What does and what does not follow from K(Fb). , 5.5. Absoluteness of A & Sigma;b & infin;-sentences of language Ln -- pt. III AC0 World -- 6. Theories I & Delta;0, I & Delta;0(R) and V01 -- 7. Shallow Boolean decision tree model -- 7.1. Family Frud -- 7.2. Family Grud -- 7.3. Properties of Frud and Grud -- 8. Open comprehension and open induction -- 8.1. The 〈〈...〉〉 notation -- 8.2. Open comprehension in K(Frud, Grud) -- 8.3. Open induction in K(Frud, Grud) -- 8.4. Short open induction -- 9. Comprehension and induction via quantifier elimination: a general reduction -- 9.1. Bounded quantifier elimination -- 9.2. Skolem functions in K(F, G) and quantifier elimination -- 9.3. Comprehension and induction for & Sigma;1,b0-formulas -- 10. Skolem functions, switching lemma and the tree model -- 10.1. Switching lemma -- 10.2. Tree model K (Ftree, Gtree) -- 11. Quantifier elimination in K(Ftree, Gtree) -- 11.1. Skolem functions -- 11.2. Comprehension and induction for & Sigma;1,b0-formulas -- 12. Witnessing, independence and definability in V01. , Machine generated contents note: Organization of the book -- Remarks on the literature -- Background -- pt. I BASICS -- 1. The definition of the models -- 1.1. The ambient model of arithmetic -- 1.2. The Boolean algebras -- 1.3. The models K (F) -- 1.4. Valid sentences -- 1.5. Possible generalizations -- 2. Measure on B -- 2.1. A metric on B -- 2.2. From Boolean value to probability -- 3. Witnessing quantifiers -- 3.1. Prepositional approximation of truth values -- 3.2. Witnessing in definable families -- 3.3. Definition by cases by open formulas -- 3.4. Compact families -- 3.5. Prepositional computation of truth values -- 4. The truth in N and the validity in K(F) -- pt. II SECOND-ORDER STRUCTURES -- 5. Structures K(F, G) -- 5.1. Language L2 and the hierarchy of bounded formulas -- 5.2. Cut Mn, languages Ln and L2n -- 5.3. Definition of the structures -- 5.4. Equality of functions, extensionality and possible generalizations.

Additional Edition: ISBN 9780521154338

Additional Edition: ISBN 9780521154338

Additional Edition: ISBN 9780521154338

Additional Edition: Erscheint auch als Krajíček, Jan, 1960 - Forcing with random variables and proof complexity Cambridge [u.a.] : Cambridge Univ. Press, 2011 ISBN 9780521154338

Additional Edition: ISBN 0521154332

Additional Edition: Erscheint auch als Druck-Ausgabe ISBN 9780521154338

Language: English

Subjects: Mathematics

Keywords: Berechnungskomplexität ; Zufallsvariable ; Beweistheorie

DOI: 10.1017/CBO9781139107211

URL: Volltext

URL: Inhaltsverzeichnis

URL: Inhaltstext

UID:

Format: XVI, 247 S. , 23 cm

Edition: 1. publ.

ISBN: 9780521154338 , 0521154332

Series Statement: London Mathematical Society lecture note series 382

Content: "This book introduces a new approach to building models of bounded arithmetic, with techniques drawn from recent results in computational complexity. Propositional proof systems and bounded arithmetics are closely related. In particular, proving lower bounds on the lengths of proofs in propositional proof systems is equivalent to constructing certain extensions of models of bounded arithmetic. This offers a clean and coherent framework for thinking about lower bounds for proof lengths, and it has proved quite successful in the past. This book outlines a brand new method for constructing models of bounded arithmetic, thus for proving independence results and establishing lower bounds for proof lengths. The models are built from random variables defined on a sample space which is a non-standard finite set and sampled by functions of some restricted computational complexity. It will appeal to anyone interested in logical approaches to fundamental problems in complexity theory"--

Content: "This book introduces a new approach to building models of bounded arithmetic, with techniques drawn from recent results in computational complexity. Propositional proof systems and bounded arithmetics are closely related. In particular, proving lower bounds on the lengths of proofs in propositional proof systems is equivalent to constructing certain extensions of models of bounded arithmetic. This offers a clean and coherent framework for thinking about lower bounds for proof lengths, and it has proved quite successful in the past. This book outlines a brand new method for constructing models of bounded arithmetic, thus for proving independence results and establishing lower bounds for proof lengths. The models are built from random variables defined on a sample space which is a non-standard finite set and sampled by functions of some restricted computational complexity. It will appeal to anyone interested in logical approaches to fundamental problems in complexity theory"--

Note: Includes bibliographical references and indexes

Additional Edition: Erscheint auch als Online-Ausgabe Krajíček, Jan Forcing with random variables and proof complexity Cambridge : Cambridge University Press, 2011 ISBN 9781139107211

Language: English

Subjects: Mathematics

Keywords: Berechnungskomplexität ; Zufallsvariable ; Beweistheorie

URL: Cover

URL: Inhaltstext

UID:

Format: 1 online resource (xvi, 247 pages) : , digital, PDF file(s).

ISBN: 9781139107211 (ebook)

Series Statement: London Mathematical Society lecture note series ; 382

Content: This book introduces a new approach to building models of bounded arithmetic, with techniques drawn from recent results in computational complexity. Propositional proof systems and bounded arithmetics are closely related. In particular, proving lower bounds on the lengths of proofs in propositional proof systems is equivalent to constructing certain extensions of models of bounded arithmetic. This offers a clean and coherent framework for thinking about lower bounds for proof lengths, and it has proved quite successful in the past. This book outlines a brand new method for constructing models of bounded arithmetic, thus for proving independence results and establishing lower bounds for proof lengths. The models are built from random variables defined on a sample space which is a non-standard finite set and sampled by functions of some restricted computational complexity. It will appeal to anyone interested in logical approaches to fundamental problems in complexity theory.

Note: Title from publisher's bibliographic system (viewed on 05 Oct 2015). , Organization of the book -- , Remarks on the literature -- , Background -- , BASICS -- , The definition of the models -- , The ambient model of arithmetic -- , The Boolean algebras -- , The models K (F) -- , Valid sentences -- , Possible generalizations -- , Measure on B -- , A metric on B -- , From Boolean value to probability -- , Witnessing quantifiers -- , Prepositional approximation of truth values -- , Witnessing in definable families -- , Definition by cases by open formulas -- , Compact families -- , Prepositional computation of truth values -- , The truth in N and the validity in K(F) -- , SECOND-ORDER STRUCTURES -- , Structures K(F, G) -- , Language L2 and the hierarchy of bounded formulas -- , Cut Mn, languages Ln and L2n -- , Definition of the structures -- , Equality of functions, extensionality and possible generalizations. , Absoluteness of A & Sigma;b & infin;-sentences of language Ln -- , AC0 World -- , Theories I & Delta;0, I & Delta;0(R) and V01 -- , Shallow Boolean decision tree model -- , Family Frud -- , Family Grud -- , Properties of Frud and Grud -- , Open comprehension and open induction -- , The ... notation -- , Open comprehension in K(Frud, Grud) -- , Open induction in K(Frud, Grud) -- , Short open induction -- , Comprehension and induction via quantifier elimination: a general reduction -- , Bounded quantifier elimination -- , Skolem functions in K(F, G) and quantifier elimination -- , Comprehension and induction for & Sigma;1,b0-formulas -- , Skolem functions, switching lemma and the tree model -- , Switching lemma -- , Tree model K (Ftree, Gtree) -- , Quantifier elimination in K(Ftree, Gtree) -- , Skolem functions -- , Comprehension and induction for & Sigma;1,b0-formulas -- , Witnessing, independence and definability in V01. , Witnessing AX〉 xEY〉 x & Sigma;1,b0-formulas -- , Preservation of true s & Pi;l, b 1-sentences -- , Circuit lower bound for parity -- , AC0(2) WORLD -- , Theory Q2V01 -- , Q2 quantifier and theory Q2V01 -- , Interpreting Q2 in structures -- , Algebraic model -- , Family Falg -- , Family Galg -- , Open comprehension and open induction -- , Quantifier elimination and the interpretation of Q2 -- , Skolemization and the Razborov-Smolensky method -- , Interpretation of Q2 in front of an open formula -- , Elimination of quantifiers and the interpretation of the Q2 quantifier -- , Comprehension and induction for Q2 & Sigma;1,b0-formulas -- , Witnessing and independence in Q2V01 -- , Witnessing AX〉 xEY〉 xAZ〉 x & Sigma;1,b0-formulas -- , Preservation of true ss & Pi;l, b 1-sentences -- , TOWARDS PROOF COMPLEXITY -- , Propositional proof systems -- , Frege and Extended Frege systems. , Language with connective and constant-depth Frege systems -- , An approach to lengths-of-proofs lower bounds -- , Formalization of the provability predicate -- , Reflection principles -- , Three conditions for a lower bound -- , PHP principle -- , First-order and propositional formulations of PHP -- , Three conditions for Fd and Fd lower bounds for PHP -- , PROOF COMPLEXITY OF FD AND FD -- , A shallow PHP model -- , Sample space & Omega;0PHP and PHP-trees -- , Structure K(F0PHP, G0PHP) and open comprehension and open induction -- , The failure of PHP in K(F0PHP, G0PHP) -- , Model K(FPHP, GPHP) of V01 -- , The PHP switching lemma -- , Structure K(FPHP, GPHP) -- , Open comprehension, open induction and failure of PHP -- , Bounded quantifier elimination -- , PHP lower bound for Fd: a summary -- , Algebraic PHP model? -- , Algebraic formulation of PHP and relevant rings -- , Nullstellensatz proof system NS and designs. , A reduction of Fd to NS with extension polynomials -- , A reduction of polynomial calculus PC to NS -- , The necessity of partially defined random variables -- , POLYNOMIAL-TIME AND HIGHER WORLDS -- , Relevant theories -- , Theories PV and ThA(LPV) -- , Theories S12, T12 and BT -- , Theories U11 and V11 -- , Witnessing and conditional independence results -- , Independence for S12 -- , S12 versus T12 -- , PV versus S12 -- , Transfer principles -- , Pseudorandom sets and a Lowenheim-Skolem phenomenon -- , Sampling with oracles -- , Structures K (Foracle) and K (Foracle, Goracle) -- , An interpretation of random oracle results -- , PROOF COMPLEXITY OF EF AND BEYOND -- , Fundamental problems in proof complexity -- , Theories for EF and stronger proof systems -- , First-order context for EF: PV and S12 -- , Second-order context for EF: VPV and V11 -- , Stronger proof systems -- , Proof complexity generators: definitions and facts. , & tau;-formulas and their hardness -- , The truth-table function -- , Iterability and the completeness of tts, k -- , The Nisan-Wigderson generator -- , Gadget generators -- , Optimal automatizer for the & tau;-formulas -- , Proof complexity generators: conjectures -- , On provability of circuit lower bounds -- , Razborov's conjecture on the NW generator and EF -- , A possibly hard gadget -- , Rudich's demi-bit conjecture -- , The local witness model -- , The local witness model K(Fb) -- , Regions of undefinability -- , Properties of the local model K(Fb) -- , What does and what does not follow from K(Fb).

Additional Edition: Print version: ISBN 9780521154338

Language: English

URL: https://doi.org/10.1017/CBO9781139107211

UID:

Format: 1 online resource (xvi, 247 pages) : , digital, PDF file(s).

ISBN: 1-107-21344-4 , 1-139-10721-6 , 1-283-29610-1 , 1-139-12308-4 , 9786613296108 , 1-139-12799-3 , 1-139-11733-5 , 1-139-11297-X , 1-139-11516-2

Series Statement: London Mathematical Society lecture note series ; 382

Content: "This book introduces a new approach to building models of bounded arithmetic, with techniques drawn from recent results in computational complexity. Propositional proof systems and bounded arithmetics are closely related. In particular, proving lower bounds on the lengths of proofs in propositional proof systems is equivalent to constructing certain extensions of models of bounded arithmetic. This offers a clean and coherent framework for thinking about lower bounds for proof lengths, and it has proved quite successful in the past. This book outlines a brand new method for constructing models of bounded arithmetic, thus for proving independence results and establishing lower bounds for proof lengths. The models are built from random variables defined on a sample space which is a non-standard finite set and sampled by functions of some restricted computational complexity. It will appeal to anyone interested in logical approaches to fundamental problems in complexity theory"--

Note: Title from publisher's bibliographic system (viewed on 05 Oct 2015). , pt. 1. Basics -- pt. 2. Second-order structures -- pt. 3. AC[superscript 0] world -- pt. 4. AC[superscript 0](2) world -- pt. 5. Towards proof complexity -- pt. 6. Proof complexity of F[subscript d] and F[subscript d]([xor]) -- pt. 7. Polynomial-time and higher worlds -- pt. 8. Proof complexity of EF and beyond. , English

Additional Edition: ISBN 0-521-15433-2

Language: English