Overview of the DIMACS Special Year on Logic and Algorithms

See Calendar of Special Year events for scheduled dates and hot links to complete calendar information.

A dichotomy in theoretical computer science is best demonstrated by looking at the 1994 Handbook of Theoretical Computer Science. Volume A discusses algorithms and complexity, while Volume B treats formal models and semantics. Theoretical computer science in the United States is largely "Vol. A"-ish, while European theoretical computer science is largely "Vol. B"-ish. The goal of this Special Year is to bridge the gap between the two branches, focusing on three bridge areas: Computer-Aided Verification, Finite-Model Theory, and Proof Complexity. All three are emerging research areas that fit naturally between Vol. A and Vol. B.

Below is a brief description of each topic, and a list of workshops associated with that topic. We also plan a series of week-long tutorials, one in each topic, intended to introduce students, recent graduates, and professionals from other areas to the topic.

Computer-Aided Verification

Computer-Aided Verification studies algorithms and structures for verifying properties of programs. It draws upon techniques from graph theory, combinatorics, automata theory, complexity theory, Boolean functions and algebras, logic, Ramsey theory and linear programming. Since the DIMACS CAV workshop in 1990, worldwide interest in CAV has grown enormously, not only in academia but in companies like Intel, DEC, SGI, Motorola, Sun and AT&T. This creates an unusual and rewarding opportunity to see theory put directly into practice. We plan workshops in "Verification and control of hybrid systems," "Partial Order Methods in Verification (POMIV)" and in "Computational and complexity issues in automated verification".

Finite-Model Theory

Model theory is the study of mathematical structures which satisfy sets of axioms. Recent work on the finite models of a set of axioms has yielded elegant connections with theoretical computer science, including model-theoretic characterizations of complexity classes. Further, when a class of finite mathematical structures (e.g. graphs) is equipped with probability measures, one can often develop powerful meta-theorems called zero-one laws, which give conditions under which probabilities must approach zero or one as the structure size goes to infinity. We plan workshops in "Finite models and descriptive complexity" and in "Logic and random structures".

Proof Complexity

Two related notions of "proof complexity" currently motivate research at the interface between computer science and logic. One notion centers on the length of a proof, and the other on the complexity of the inference steps within the proof. It is well known that NP=co-NP iff all propositional tautologies have short proofs. But the connection between proof length and complexity theory goes much deeper. Lower bounds on circuits are closely tied to those on proof length in restricted systems, and advances on one front often lead quickly to progress on the other. By restricting the complexity of inference steps within a proof, one obtains a fragment of Peano Arithmetic called Bounded Arithmetic, which defines exactly the predicates in the polynomial hierarchy. Exciting recent work has shown that if certain theories of bounded arithmetic can prove lower bounds in complexity theory, then corresponding cryptographic systems cannot be secure. We plan a single, four-day workshop on "Feasible arithmetic and lengths of proofs".

Other Workshops

Additional workshops are planned and under consideration.

A workshop on the "Satisfiability Problem: Theory and Applications" examines the strong relationship between the theory, algorithms, and the applications of the SAT problem. he main focus of this workshop is to bring together the best theorists, algorithmists, and practitioners working on the SAT problem and on the industrial applications involving the SAT problem, enhancing the interaction between the three research groups. As an important activity of the workshop, a set of SAT problem benchmarks derived from the practical industrial engineering applications will be provided for SAT algorithm benchmarking.

Summer School on Applied Logic

The Summer School is intended to expose industry, graduate students, postdocs, and experienced researchers from other fields to the three focus areas of the Special Year --- Finite-Model Theory, Proof Complexity, and Computer-Aided Verification. It will consist of three consecutive one week tutorials. The courses will provide students with a deep understanding of these research areas and will point out connections with applications.

Postdoctoral Fellows

DIMACS and AT&T Bell Labs will have five postdoctoral fellows for 1995-96. They are:

Distinguished Lecturer Series

The special year will sponsor a series of five distinguished lecturer talks. The speakers are:

Other Interactions

As usual, this DIMACS Special Year aims to be inclusive, not exclusive. Many other areas, beyond the organizers' ken, would mesh with these themes. This fourth, "catch-all" topic is intended to encourage all scientists who might benefit from interaction with logicians, combinatorialists and computer scientists, and with the topics we HAVE listed.

Federated Logic Conference

As part of this Special year, DIMACS will host a Federated Logic Conference (FLC). FLC will be modeled after the successful Federated Computer Research Conference (FCRC). The goal is to battle fragmentation of the technical community by bringing together synergetic conferences that apply logic to computer science. The following conferences will participate in FLC: CADE (Conference on Automated Deduction), CAV (Conference on Computer-Aided Verification), LICS (IEEE Symp. on Logic in Computer Science), and RTA (Conference on Rewriting Techniques and Applications). The four conferences will span eight days, with only two-way parallelism at any given time. We will make special efforts to bring about interaction between the various conferences. The meeting will take place in late July, 1996, on one of the Rutgers campuses.

For Further Information

Special Year Organizing Committee:

Special Year Publicity Chair:

Special Year Steering Committee:

Special Year Industrial Advisory Board

IndexIndex of Special Year on Logic and Algorithms
DIMACS Homepage
Contacting the Center
Document last modified on October 19, 1998.