(Message inbox:46) Return-Path: Received: from CS.CMU.EDU by MISSING.LINK.CS.CMU.EDU id aa04164; 6 Mar 96 10:56 EST Received: from hearn.nic.surfnet.nl by CS.CMU.EDU id aa28558; 6 Mar 96 10:53:21 EST Received: from HEARN.NIC.SURFNET.NL by HEARN.nic.SURFnet.nl (IBM VM SMTP V2R2) with BSMTP id 3712; Wed, 06 Mar 96 16:46:44 +0100 Received: from NIC.SURFNET.NL (NJE origin LISTSERV@HEARN) by HEARN.NIC.SURFNET.NL (LMail V1.2a/1.8a) with BSMTP id 3105; Wed, 6 Mar 1996 16:46:32 +0100 Received: from NIC.SURFNET.NL by NIC.SURFNET.NL (LISTSERV release 1.8b) with NJE id 9521 for DMA-LIST@NIC.SURFNET.NL; Wed, 6 Mar 1996 16:46:20 +0100 Received: from HEARN (NJE origin SMTP@HEARN) by HEARN.NIC.SURFNET.NL (LMail V1.2a/1.8a) with BSMTP id 3091; Wed, 6 Mar 1996 16:46:19 +0100 Received: from utmfu0.math.utwente.nl by HEARN.nic.SURFnet.nl (IBM VM SMTP V2R2) with TCP; Wed, 06 Mar 96 16:46:04 +0100 Received: by utmfu0.math.utwente.nl ($Revision: 1.36.108.11 $/16.2) id AA075157067; Wed, 6 Mar 1996 16:44:28 +0100 Full-Name: DMANET Mailer: Elm [revision: 66.36.1.1] Approved-By: DMANET Message-ID: <199603061544.AA075157067@utmfu0.math.utwente.nl> Date: Wed, 6 Mar 1996 16:44:25 MET Reply-To: DMANET Sender: DMANET From: DMANET Subject: DIMACS Workshop on Feasible Arithmetics and Length of Proofs, April 21-23, 1996, DIMACS Center, Co To: Multiple recipients of list DMA-LIST DIMACS Special Year on Logic and Algorithms DIMACS Workshop on Feasible Arithmetics and Length of Proofs April 21 - 23, 1996 DIMACS Center, CoRE Building Rutgers University Organizers:Paul Beame and Sam Buss E-Mail: beame@cs.washington.edu and sbuss@cs.ucsd.edu This workshop will cover two complementary approaches to the complexity of proving a mathematical fact, with emphasis on their connections to circuit complexity and computational complexity. Feasible theories of arithmetic are weak first- or second-order systems whose theorems correspond to problems in computational classes such as the levels of the polynomial time hierarchy or the NC hierarchy. The ``length of proofs'' approach, on the other hand, studies the growth rate (in number of symbols, number of lines, logical depth, etc.) of proofs of instances of some theorem within a fixed, quantifier-free proof system. Proof complexity and feasible arithmetics are closely related to each other and to fundamental problems from circuit complexity and computational complexity, such as the NP versus coNP problem. Over the last decade there has been significant progress in the study of these areas and many deep connections between them have been discovered. One example is the application of methods from circuit complexity lower bound proofs to obtain new lower bounds on proof complexity. Another example is the recent work on natural proofs, which has shown that if certain theories of bounded arithmetic can prove lower bounds in complexity theory, then certain levels of cryptographic security cannot be achieved. The workshop will emphasize the interconnections among proof complexity, arithmetic complexity and computational complexity. This encompasses a broad range of topics of current interest, including Frege systems, bounded depth proof systems, cutting plane and Nullstellensatz proof systems, switching lemmas, recursion theoretic characterizations of complexity classes, bounded arithmetic and other feasible formal systems, cryptographic conjectures, interpolation theorems, independence results, interpretability and conservativity. ____________________________________________________________________________ WORKSHOP on FEASIBLE ARITHMETICS AND PROOF COMPLEXITY Sunday, April 21 - Location: Holiday Inn, Plainfield, N.J. ---------------- 9:00-10:00 - Toniann Pitassi Simplified Lower Bounds for Resolution 10:00-10:30 - Coffee break. 10:30-11:30 - Steven Rudich "Natural Proofs - A Survey, Part I." 11:30-12:00 - Peter Clote (joint with A. Setzer) "A note on Degen's principle and odd charged graphs" 12:00-1:00 - Lunch, provided by the conference organizers. 1:30-2:30 - Daniel Leivant TBA 2:30-3:00 - Sam Buss TBA 3:00-3:45 - Coffee break. 3:45-4:15 - Ken Regan "Descriptive Complexity and the W Hierarchy." 4:15-4:45 - Mario Chiari "A Further Look at the Provably Total Functions of S^w_2." 7:00-9:00 - Reception. Monday, April 22 - DIMACS, Rutgers, N.J. ---------------- 9:00-10:00 - Russell Impagliazzo "Algebra, Proofs and Algorithms" 10:00-10:30 - Coffee break. 10:30-11:30 - Alexander A. Razborov "Proof Complexity in Algebraic Systems and Constant Depth Frege Proofs." 11:30-12:00 - Steven Rudich "Natural Proofs - A Survey, Part II." 12:00-1:00 - Lunch, provided by the conference organizers. 1:30-2:30 - Pavel Pudlak "Monotone Circuits and Propositional Calculus." 2:30-3:00 - Xudong Fu "Lower Bounds on the Size of Cutting Planes Proofs for Modular Coloring Principles." 3:00-3:45 - Coffee break. 3:45-4:15 - Fernando Ferreira "A Proof that LogSpace is not equal to NLin." 4:15-4:45 - Barbara Kaufman "Bounded Arithmetic: Comparion of Herbrand Analysis and the Witnessing Method." 4:45-5:15 - Open Problems Session/Short talk Tuesday, April 23 - DIMACS, Rutgers, N.J. ----------------- 9:00-10:00 - Jan Krajicek "Model Theory Related to Lengths of Proofs." 10:00-10:30 - Coffee break. 10:30-11:30 - Gaisi Takeuti "Incompleteness Theorems, Forcing and P=/=NP." 11:30-12:00 - Dan Willard "Self-Justifying Axiom Systems, Their Reflection Principles and Possible Connections to NP." 12:00-1:00 - Lunch, provided by conference organizers 1:30-2:00 - Jeremy Avigad "Plausibly Hard Tautologies?" 2:00-3:00 - Paul Beame TBA 3:00-3:45 - Coffee break. 3:45-4:15 - Steven Bellantoni "Ramification and Feasibility." 4:15-4:45 - Reserved for short talk. -- ****************************************************** Contributions to be spread via DMANET are submitted to DMANET@math.utwente.nl Replies to a message carried on DMANET should NOT be addressed to DMANET but to the original sender. The original sender, however, is invited to prepare an update of the replies received and to communicate it via DMANET. DISCRETE MATHEMATICS AND ALGORITHMS NETWORK (DMANET)