[ Guideline for preparing your final version ]
[ Registration form: Ascii, PS, MS-Word ]
[ Hotel reservation: Ascii, PS, MS-Word ]
[ Schedule: TeX, PS ]


International Workshop on
First order Theorem Proving

Schloss Hagenberg, Austria
October 27 - 28, 1997

Scope of the workshop

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 that bridge the areas of theorem proving and constraints (e.g., in the areas of equational reasoning, term rewriting systems, and satisfiability problems) are especially welcome.

Technical Program

The technical program includes presentations of the accepted papers and an invited talk by Bruno Buchberger (RISC Linz) entitled 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 Contraint Programming (CP97), 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; for information on double registration see the registration form (Ascii, Postscript, or MS-Word).

Conference Venue

Schloss Hagenberg, the home of the Research Institute for Symbolic Computation (RISC-Linz), is a renovated, medieval castle, in the lovely landscape of the hills surrounding the city of Linz, Austria.

Final version of accepted papers

Final versions are due by September 30, 1997; this is a firm deadline.

The paper should be written in 11-point font size with a text area of 15 x 23 cm (= 5.91 x 9.06 in). The top margin should be 3.4 cm (= 1.34 in), the left margin should be 3 cm (= 1.18 in). Page numbers should appear centered below the text. The page limit is 5 pages. Preferably, the paper should be typeset with LaTeX.

The camera-ready copy has to be sent as uuencoded gzipped Postscript file by electronic mail to ftp97@logic.at.

For further informations see the final version guideline or send an email to salzer@logic.at.


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 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.


Please complete the registration form (Ascii, PS, MS-Word) and the hotel reservation form (Ascii, PS, MS-Word) and send them by e-mail, fax or surface mail to:

Betina Curtis
RISC - Research Institute for Symbolic Computation
Schloss Hagenberg
A-4232 Hagenberg
Fax: +43(7236)323130
E-mail: bcurtis@risc.uni-linz.ac.at
Note that there is a discount for registering simultaneously for FTP97 and CP97, as well as an extra charge for registering after September 30; see the registration form for details.

Conference Organization

Program Committee:

Wolfgang Bibel (Technische Hochschule Darmstadt)
Maria Paola Bonacina (University of Iowa) (co-chair),
Ulrich Furbach (Universität Koblenz) (co-chair), uli@mailhost.uni-koblenz.de
Ryuzo Hasegawa (Kyushu University)
Alexander Leitsch (Technische Universität Wien)
Reinhold Letz (Technische Universität München)
Christopher Lynch (Clarkson University)
Neil Murray (SUNY at Albany)
David Plaisted (UNC at Chapel Hill)
Michael Rusinowitch (INRIA-Lorraine)

Local Arrangements Chair:

Gernot Salzer (Technische Universität Wien), salzer@logic.at

Steering Committee:

David Plaisted (UNC at Chapel Hill) (chair)
Maria Paola Bonacina (University of Iowa)
Ulrich Furbach (Universität Koblenz)
Jieh Hsiang (National Taiwan University)
Christopher Lynch (Clarkson University)
Xumin Nie (Wichita State University)
Michael Rusinowitch (INRIA-Lorraine)
Gernot Salzer (Technische Universität Wien)
Camilla Schwind (Université Aix-Marseille II)
Klaus Trümper (University of Texas at Dallas)
Hantao Zhang (University of Iowa)

Important dates

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

Last modification on 26 October 97 by
G. Salzer