The 17th International Conference on Automated Deduction June 17-20, 2000, Pittsburgh, Pennsylvania, USA PRELIMINARY CALL FOR PAPERS (further details at http://www.research.att.com/conf/cade) For the last 25 years CADE has been the major forum for the presentation of research in automated deduction. Original research papers in all aspects of automated theorem proving, automated reasoning, computer aided verification, formal methods and static analysis are solicited for CADE-17. PROGRAM CHAIR: David McAllester, AT&T Labs-Research CONFERENCE CHAIR: Frank Pfenning, Carnegie Mellon University PROGRAM COMMITTEE: Hubert Comon, David Dill, Ulrich Furbach, Harald Ganzinger, Mike Gordon, Didier Galmiche, Tom Henzinger, Deepak Kapur, Ursula Martin, Ken McMillan, Paliath Narendran, David Plaisted, Robert Nieuwenhuis, Tobias Nipkow, Hans de Nivelle, Larry Paulson, Amir Pnueli, Mark Stickel, Moshe Y. Vardi, Andrei Voronkov. SUBMISSIONS DEADLINE: January 15, 2000 NOTIFICATION OF ACCEPTANCE: March 1 CAMERA-READY COPY: March 21 SUBMISSIONS: Papers must be original and not submitted for publication elsewhere. Research papers can be up to 15 proceedings pages, and system descriptions can be up to 5 pages. System description submissions must include a URL for a web page from which the system can either be run or obtained by reviewers. The proceedings of CADE-17 will be published by Springer-Verlag in the LNAI series. Electronic submission of postscript generated from LaTeX2e and the Springer llncs class files is strongly encouraged (details and alternatives at the web site above).