Delivery-Date: 
From: Johann Schumann <schumann@informatik.tu-muenchen.de>
To: qed@mcs.anl.gov
Subject: CADE-13 Call for Papers
Message-Id: <95Aug31.113309+0200mesz.460951+162@sunjessen21.informatik.tu-muenchen.de>
Date: Thu, 31 Aug 1995 11:32:59 +0200
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


     The Thirteenth International Conference on Automated Deduction
     --------------------------------------------------------------

			    Rutgers University
		      New Brunswick, New Jersey, USA

			 30 July - 3 August, 1996

		         CADE-13:  First Call for Papers

The CADE conferences are the major forum for the presentation of new
research in all aspects of automated deduction. Original research
papers, descriptions of working reasoning systems, and problem sets
that provide innovative, challenging tests for automated reasoning
systems, are solicited.

CADE conferences cover all aspects of automated deduction:

    First vs. Higher Order Logics            Classical vs. Non-Classical Logics
    Special vs. General Purpose Inference    Interactive vs. Automatic Systems

Specific topics of interest include (but are not limited to):

    Resolution		Sequent Calculus        Decision Procedures
    Unification		Rewrite Rules           Mathematical Induction

and any applications of automated deduction, including:

    Deductive Databases         Logic and Functional Programming
    Commonsense Reasoning       Software and Hardware Development

******************************************************************
** Papers on commercial or industrial applications of automated **
** deduction are especially encouraged.				**
******************************************************************

CADE-13 will be held from Tuesday 30 July, to Saturday, 3 August. It
will be held as part of the Federated Logic Conference (FLoC'96) to be
held at Rutgers University, New Brunswick, New Jersey, USA, from
Saturday, July 27, to Saturday, August 3. As well as CADE, other
conferences participating in FLoC'96 will be CAV (Conference on
Computer-Aided Verification), LICS (IEEE Symposium on Logic in Computer
Science), and RTA (Conference on Rewriting Techniques and
Applications). The goal of FLoC is to battle fragmentation of the
technical community by bringing together synergetic conferences that
relate logic to computer science.

The Proceedings of CADE-13 will be published by Springer-Verlag in
their Lecture Notes in Artificial Intelligence Series. Research papers
should not exceed 15 (fifteen) proceedings pages. System descriptions
and problem sets should not exceed 5 (five) proceedings pages. Springer
style files should be used if possible. These can be obtained early
September from http://www.research.att.com/lics/FLoC.

The title page of the submission should include the name, address (with
email address if possible) and telephone number of each author. To
assist in the refereeing process, please indicate one or at most two of
the following areas into which your paper falls, or if it does not fall
into any of these areas, please specify the area into which it falls:

	LOGIC: first order, higher order, classical, non-classical,
	constructive, type theory, induction, modal, non-monotonic.

	MECHANISMS: resolution, matrix, sequent calculus, natural
	deduction, semantic tableau, rewrite rules, unification,
	decision procedures, tactics, meta-level, interactive,
	analogy.

	APPLICATIONS: mathematics, geometry, databases, logic
	programming, functional programming, software/hardware
	verification/transformation/synthesis/termination, commonsense
	reasoning, expert systems, learning.

Papers must be unpublished and not submitted for publication
elsewhere. Submissions which are late, too long, or which require
major revision, will not be considered.

The Program Committee may ask authors to furnish evidence of
scientific claims, eg computer programs, detailed proofs, or full
experimental data.

          +-----------------------------------------------+
          | Submission deadline: 12 January, 1996         |
          | Notification of acceptance: 20 March, 1996    |
          | Camera-ready copy due: 26 April, 1996         |
          +-----------------------------------------------+

Authors should send 4 (four) copies of their submission to the Program
Co-Chairs. Further information about the conference may be obtained
from the Local Arrangements Chair or at the CADE-13 world wide web
site: http://www.research.att.com/lics/FLoC (operational early
September).

Further calls will be made for tutorials, workshops and a theorem
proving competition and details of these will also be available at the
CADE-13 web site.

        Program Co-Chairs              		Local Arrangements Chair

        Michael McRobbie & John Slaney		Amy Felty		
	Centre for Information			AT&T Bell Laboratories
          Science Research			600 Mountain Avenue 
	The Australian National University	Murray Hill NJ 07974
	ACT 0200				United States of America
	Australia
                                     
        Tel: [+61] 6-2492035			Tel: [+1] 908-5824049 
        Fax: [+61] 6-2490747       		Email: cade13-la@cisr.anu.edu.au
        Email: cade13@cisr.anu.edu.au

			Program Committee

O. Astrachan (Duke)			J. Avenhaus (Kaiserslautern)
L. Bachmair (Stonybrook)       		D. Basin (Max-Planck)
W. Bibel (Darmstadt)			B. Buchberger (Linz)
F. Bry (Munich)				R. Caferra (Grenoble)
K.S. Choi (KAIST)			A. Cohn (Leeds)
L. Farinas del Cerro (Toulouse)		W. Farmer (MITRE)
A. Felty (AT&T)				M. Fitting (CUNY)
M. Fujita (MRI)				S. Garland (MIT)
F. Giunchiglia (IRST)			E. Gunter (AT&T)
R. Hasegawa (Kyushu)			L. Henschen (North Western)
L. Hines (Texas)			S. Hoelldobler (Dresden)
M. Kaufman (Motorola)			A. Leitsch (Vienna)
E. Lusk (Argonne)			U. Martin (St Andrews)
D. McAllester (MIT)			W. McCune (Argonne)
H.-J. Ohlbach (Max-Planck)		J. Posegga (Karlsruhe)
W. Pase (Ottawa)			F. Pfenning (Carnegie Mellon)
F. Pirri (Rome)				D. Plaisted (North Carolina)
U. Reddy (Illinois)			M. Rusinowitch (INRIA)
K. Satoh (Hokkaido)			J. Schumann (Munich)
C. Schwind (Marseille)			N. Shankar (SRI)
J. Siekman (Saarbruecken)		A. Smaill (Edinburgh)
G. Smolka (Saarbruecken)		M. Stickel (SRI)
G. Sutcliffe (James Cook)		E. Tiden (Siemens)
A. Voronkov (Uppsala)			L. Wallen (Oxford)
D. Wang (Grenoble)			H. Zhang (Iowa)

----- End Included Message -----