%
%                         Call for Papers - FTP97
%
%       International Workshop on First-Order Theorem Proving (FTP97)
%               http://www.logic.at/FTP97/
%
%               Schloss Hagenberg, near Linz (Austria)
%                         October 27-28, 1997
%
\documentstyle{article}
%
\newif\ifPubChair
%\PubChairtrue% Uncomment this line to include a Pub Chair
%
\oddsidemargin -1.4cm  %%% Ok for both A4 and US letter paper
\topmargin -1cm        %%% This is for A4 paper only
%\topmargin -1.7cm        %%% This is for US letter paper only
\textwidth  18.5cm
\textheight 27cm
\headheight 0pt
\headsep 0pt 
\footheight 0pt
\footskip 0pt
\parindent 0pt
\def\vsep{3ex}
\pagestyle{empty}
\begin{document}

\begin{center}
{\Large\sc  Call for Papers -- FTP97}\\[2.5ex]
{\Large \bf International Workshop on
            First-Order Theorem Proving (FTP97)}\\[1.5ex]
{\large\bf  Schloss\ Hagenberg, Austria, October 27--28, 1997}\\[1.5ex]
{\large\tt  http://www.logic.at/FTP97}\\[5ex]
\end{center}

\parbox[t]{7.4cm}{\small
%
{\bf Program Chairs:}\\[1.5ex]
%
\begin{tabular}{l}
Maria Paola Bonacina\\
University of Iowa\\
{\tt bonacina@cs.uiowa.edu}\\[1ex]
Ulrich Furbach\\
Universit\"at Koblenz\\
{\tt uli@mailhost.uni-koblenz.de}
\end{tabular}\\[3ex]
%
{\bf Program Committee:}\\[1.5ex]
%
\begin{tabular}{l}
Wolfgang Bibel (Techn.~Hochschule Darmstadt)\\
Maria Paola Bonacina (University of Iowa)\\
Ulrich Furbach (Universit\"at Koblenz)\\
Ryuzo Hasegawa (Kyushu University)\\
Alexander Leitsch (Techn.~Universit\"at Wien)\\
Reinhold Letz (Techn.~Universit\"at M\"unchen)\\
Christopher Lynch (Clarkson University)\\
Neil Murray (SUNY at Albany)\\
David Plaisted (UNC at Chapel Hill)\\
Michael Rusinowitch (INRIA-Lorraine)
\end{tabular}\\[3ex]
%
{\bf Local Arrangements Chair:}\\[1.5ex]
%
\begin{tabular}{l}
Gernot Salzer\\
Technische Universit\"at Wien\\
{\tt salzer@logic.at}
\end{tabular}\\[3ex]
%
\ifPubChair
{\bf Publicity Chair:}\\[1.5ex]
%
\begin{tabular}{l}
Name\\
University\\
{\tt e-mail address}
\end{tabular}\\[3ex]
\fi
%
{\bf Steering Committee:}\\[1.5ex]
%
\begin{tabular}{l}
David Plaisted (chair) (UNC at Chapel Hill)\\
Maria Paola Bonacina (University of Iowa)\\
Ulrich Furbach (Universit\"at Koblenz)\\
Jieh Hsiang (National Taiwan University)\\
Christopher Lynch (Clarkson University)\\
Xumin Nie (Wichita State University)\\
Michael Rusinowitch (INRIA-Lorraine)\\
Gernot Salzer (Techn.~Universit\"at Wien)\\
Camilla Schwind (Universit\'e Aix-Marseille II)\\
Klaus Tr\"umper (University of Texas at Dallas)\\
Hantao Zhang (University of Iowa)
\end{tabular}\\[3ex]
%
{\bf Important dates:}\\[1.5ex]
\begin{tabular}{ll}
   August 27, 1997 & Paper submissions\\
   September 15, 1997 & Acceptance notification\\
   September 30, 1997 & Camera-ready copy due\\
   October 27--28, 1997 & FTP97\\
   October 29--31, 1997 & CP97 Main program\\
   November 1, 1997 & CP97 Workshops 
\end{tabular}
}
%
\parbox[t]{5mm}{
\rule[-23cm]{0.2mm}{23.3cm}
}
%
\begin{minipage}[t]{10.43cm}
\small
{\bf Scope:}
The workshop is intended to focus effort on First-Order Theorem Proving
as a core theme of Automated Deduction, and to provide a forum for 
presentation of very recent work and discussion of research in progress.

The workshop welcomes original contributions on theorem proving in 
first-order logics, including resolution and tableau methods; equational
reasoning and term-rewriting systems; constraint-based reasoning; 
unification algorithms for first-order theories; specialized decision 
procedures; propositional logic; abstraction; first-order constraints; 
complexity of theorem proving procedures; and applications of first-order
theorem provers to problems in artificial intelligence, verification, 
mathematics, as well as other areas. Papers bridging the areas of theorem
proving and constraints (e.g., in the areas of equational reasoning, 
term rewriting systems, and satisfiability problems) are especially 
welcome.%
\vspace{\vsep}

{\bf Technical Program:}
The technical program will include presentations of the accepted papers
and an invited talk by Bruno Buchberger (RISC Linz) entitled
             {\em The Theorema Project: An Overview}.
There will be ample time for questions and discussions in an informal
atmosphere to foster the exchange of new ideas.

The Workshop is held right before CP97, the International Conference on
Constraint Programming, which will be in the same location on 
October 29,~30, and~31, with post-conference workshops on November~1.
Theorem proving is one of the disciplines which have contributed to the
growth of constraints as a representational and computational paradigm
of wide application in Computer Science. In turn, the advances in the
field of constraints are important to theorem proving. The organization
of the two events in sequence is meant to represent an opportunity for
cross-fertilization of ideas between the two neighboring fields.

Attendance of both events is strongly encouraged (information on double
registration will be available in the calls for participation of both
FTP97 and CP97). More information on CP97 can be found at
{\tt http://www.mpi-sb.mpg.de/conferences/CP97}.%
\vspace{\vsep}

{\bf Conference venue:}
Schloss Hagenberg, the home of the Research Institute for Symbolic
Computation (RISC), is a renovated, medieval castle, in the lovely
landscape of the hills surrounding the city of Linz, Austria.
\vspace{\vsep}

{\bf Submissions:}
Authors are invited to submit an extended abstract of up to 5 pages,
with font size not smaller than 11pt, as uuencoded gzipped
Postscript files, preferably produced by \LaTeX,
sent by electronic mail to {\tt ftp97@cs.uiowa.edu}.
(See the FTP97 home page for instructions.) 
The first page should contain the
title, authors, e-mail and postal addresses of the authors.
Extended abstracts of papers published or submitted elsewhere
are not acceptable.

The submission deadline is August~27, 1997. This is a firm deadline.
Decisions on acceptance will be sent by September~15, 1997.
The deadline for sending the final versions of the extended abstracts
is September~30, 1997. This also is a firm deadline.%
\vspace{\vsep}

{\bf Publication:}
The extended abstracts that are accepted will be collected in a Technical
Report of RISC-Linz, which will be distributed at the workshop.
A special issue of the Journal of Symbolic Computation, entitled
{\em Recent Advances in First-Order Theorem Proving}, is being planned.
The authors of accepted extended abstracts will have the possibility of
submitting a full version of their papers to the special issue.
More information on this special issue, including the deadline for 
submission of the full papers, will be announced at or after the 
workshop.
\vspace{\vsep}

{\bf Additional~information} 
will be available at the
FTP97 web site: \ {\tt http://www.logic.at/FTP97}.
\end{minipage}
\end{document}