Workshop Participants and Observers
Peter Andrews (Carnegie Mellon University) Wolfgang Bibel (Technische Hochschule Darmstadt, Germany) Robert Boyer (University of Texas, Austin) Shang-Ching Chou (The Wichita State University) Edmund Clarke (Carnegie Mellon University) Robert Constable (Cornell University) Nachum Dershowitz (University of Illinois) Xiao-Shan Gao (The Wichita State University) Elsa Gunter (AT&T Bell Laboratories) Lawrence Henschen (Northwestern University) Deepak Kapur (State University of New York at Albany) Matt Kaufmann (Motorola Corporation, Austin) Kenneth Kunen (University of Wisconsin, Madison) Donald Loveland (Duke University) Michael Lowry (NASA Ames Research Center) Ewing Lusk (Argonne National Laboratory) William McCune (Argonne National Laboratory) Ross Overbeek (Argonne National Laboratory) Natarajan Shankar (SRI International) Mark Stickel (SRI International) Richard Waldinger (SRI International) Larry Wos (Argonne National Laboratory) Hantao Zhang (University of Iowa) Xudong Zhao (Carnegie Mellon University)
Observers from the National Science Foundation:
Kamal Abdali (Program Director, Numeric, Symbolic and Geometric Computation, Division of Computer and Computation Research) Richard Kieburtz (Division Director, Division of Computer and Computation Research)
Automated Deduction in the United States and Europe: An Observation
Funding of research in the automated deduction (AD) field in the United States has declined relative to the funding of AD research in Europe over the past decade. The effect of the shift in relative funding levels is reflected in the number of contributors of papers to the premier conference of the field, the Conference on Automated Deduction (CADE). The table given here reports the percentage of authors from the United States, Europe, and other locales for the CADE conferences of the past decade through 1996.
Funding of AD research in the United States traditionally has come from two sources: the Defense Department and the National Science Foundation (NSF). The Defense Department's interest centers on automated verification of hardware and software systems. This interest peaked in the 1970s and has declined steadily since that decade. Figures for the support levels are not available. The NSF support has been almost constant over the past decade at roughly $1 million in the Numeric, Symbolic and Geometric Computation program, the core program for support of AD research. This support is often augmented by cost sharing from the AI, software engineering, and logic programs of NSF, which provides up to 25% in additional funds.
Support for AD research in Europe has increased substantially in the past decade, primarily in Germany. Support has been present in Europe since the 1950s, with strong work done in France, Germany, and the United Kingdom in particular. (The University of Edinburgh was one of the first centers of AD research.) The recent increase in support comes primarily in Germany, with the centerpiece being the DFG Schwerpunktprogramm Deduktion. This program spans the years 1992-1998 and provides approximately $2-$3 million per year (U.S. dollars equiv.) for basic AD research, with a special interest in applications to programming. There is increased support in other countries but nothing as large or identifiable as the increase in Germany.
|1992||44%||49%||7%||Saratoga Springs, NY|
|1996||19%||79%||2%||New Brunswick, NJ|
Source of Table: Automated Deduction as an International Discipline--An open letter to the president of CADE, in Association for Automated Reasoning Newsletter 35, December 1996. The letter was authored by Pierre Lescanne (Nancy, France) and Christoph Walther (Darmstadt, Germany). Some text regarding sites has been altered.