CADE-14 Call for Attendance
To: firstname.lastname@example.org (German Deduction Group Research), email@example.com (MIT AI list Research), firstname.lastname@example.org (Interest Group on Propositional and Predicate Logics Research), email@example.com (Types mailing list Research), firstname.lastname@example.org (Stanford Logic Research), email@example.com (Australiasian Association for Logic Research), firstname.lastname@example.org (Rewriting Group Research), email@example.com (QED Research), firstname.lastname@example.org (German Group \(ATP\) Research)
Subject: CADE-14 Call for Attendance
From: Geoff Sutcliffe <email@example.com>
Date: Fri, 14 Feb 1997 15:46:12 +1000 (EST)
Delivery-Date: Fri, 14 Feb 1997 00:49:17 -0500
The 14th International Conference on Automated Deduction
July 13-17, 1997, Townsville, Australia
CALL FOR ATTENDANCE
Program Committee CADE is the major forum for presentation of
L. Bachmair (Stony Brook) research in all aspects of automated deduction.
H. Comon (Orsay) Logics of interest include propositional, first
W. Farmer (Bedford) order, equational, higher order, classical,
M. Fujita (Tokyo) intuitionistic, constructive, type theory,
H. Ganzinger (Saarbruecken) nonstandard, and meta-logics. Methods of interest
F. Giunchiglia (Trento) include resolution, paramodulation, unification,
J. Harrison (Turku) term rewriting, tableaux, constraints, decision
R. Hasegawa (Kyushu) procedures, induction, interactive systems, and
S. Hoelldobler (Dresden) frameworks. Applications of interest include
J. Hsiang (Taipei) hardware and software development, systems
D. Kapur (Albany) verification, artificial intelligence, logic, set
C. Kirchner (Nancy) theory, mathematics, applicative programming, and
C. Kreitz (Cornell) logic programming. Special topics of interest
A. Leitsch (Vienna) include proof translation, human-computer
R. Letz (Munich) interfaces, distributed deduction, and search
E. Lusk (Argonne) heuristics.
U. Martin (St. Andrews)
D. McAllester (Murray Hill) CADE-14 will be held from 13th to 17th July 1997,
W. McCune (Argonne) at the Sheraton Breakwater Hotel, in Townsville,
L. Paulson (Cambridge) North Queensland, Australia (i.e., in the
F. Pfenning (Pittsburgh) sunshine, near the Great Barrier Reef). The
M. Rusinowitch (Nancy) conference will be hosted by the Department of
J. Schumann (Munich) Computer Science at James Cook University of
N. Shankar (Menlo Park) North Queensland. CADE-14 features:
J. Slaney (Canberra)
M. Stickel (Menlo Park) + Six full day workshops (13th July)
G. Sutcliffe (Townsville) + Four half day tutorials (13th July)
T. Tammet (Goeteborg) + Twenty five research papers (14th-17th July)
A. Voronkov (Uppsala) + Seventeen system descriptions (14th-17th July)
L. Wallen (Oxford) + A banquet on Magnetic Island (16th July)
C. Walther (Darmstadt) + An excursion to the Great Barrier Reef
D. Wang (Grenoble) (18th July)
H. Zhang (Iowa City)
You are invited to attend CADE-14, to participate
in the high quality technical program, and to
enjoy some great social events.
Information and Registration
Full details about CADE-14 and an electronic registration form are on the WWW:
Alternatively, send us email (firstname.lastname@example.org) or a FAX (+61 77 215515),
and all the information will be sent to you. Note: No hardcopy information or
registration forms will be distributed unless explicitly requested.
Early registration deadline: May 12, 1997
Program Chair: Local Arrangements Chair:
William McCune Geoff Sutcliffe
Argonne National Laboratory James Cook University
Phone: +1 630 252 3065 Phone: +61 77 815085
FAX: +1 630 252 5986 FAX: +61 77 814029
E-mail: email@example.com E-mail: firstname.lastname@example.org
CADE-14 Advance Program Summary
+ Automated Induction Theorem Proving
+ Strategies in Automated Deduction
+ Automated Theorem Proving in Software Engineering
+ Automated Theorem Proving and Mathematics
+ Connectionist Systems for Knowledge Representation and Deduction
+ AI Methods in Theorem Proving
+ Learning from Previous Proof Experience
+ Deduction Methods Based on Boolean Rings
+ Term Indexing in Automated Reasoning, Databases and Declarative Programming
+ Higher Order Equational Logic
+ Professor Wu Wen-Tsun, Academia Sinica, Beijing, China
+ Professor Moshe Vardi, Rice University, Houston, USA
+ Decidable Call by Need Computations in Term Rewriting.
Irene Durand, Aart Middeldorp
+ A New Approach for Combining Decision Procedures for the Word Problem, and
Its Connection to the Nelson-Oppen Combination Method.
Franz Baader, Cesare Tinelli
+ On Equality Up-to Constraints over Finite Trees, Context Unification and One-
Joachim Niehren, Manfred Pinkal, Peter Ruhrberg
+ A Practical Symbolic Algorithm for the Inverse Kinematics of 6R Manipulators
with Simple Geometry.
Lu Yang, Hongguang Fu, Zhenbing Zeng
+ Automatic Verification of Cryptographic Protocols with SETHEO.
+ A Practical Integration of First-Order Reasoning and Decision Procedures.
Nikolaj S. Bjorner, Mark E. Stickel and Tomas E. Uribe
+ Some Pitfalls of LK-to-LJ Transformations and How to Avoid Them.
+ Deciding Intuitionistic Propositional Logic via Translation into Classical
Daniel Korn, Christoph Kreitz
+ Lemma Matching for a PTTP-based Top-down Theorem Prover.
+ Exact Knowledge Compilation in Predicate Calculus: the Partial Achievement
Olivier Roussel, Philippe Mathieu
+ Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem
Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta and Miyuki Koshimura
+ Connection-Based Proof Construction in Linear Logic.
Christoph Kreitz, Heiko Mantel, Jens Otten, Stephan Schmitt
+ Resource-distribution via Boolean Constraints.
James Harland, David Pym
+ Constructing a Normal Form for Property Theory.
Mary Cryan, Allan Ramsay
+ Using a Generalisation Critic to Find Bisimulations for Coinductive Proofs.
Louise Dennis, Alan Bundy, Ian Green
+ A Colored Version of the lambda-Calculus.
Dieter Hutter, Michael Kohlhase
+ A Practical Implementation of Simple Consequence Relations Using Inductive
+ Soft Typing for Ordered Resolution.
Harald Ganzinger, Christoph Meyer, Christoph Weidenbach
+ A Classification of Non-Liftable Orders for Resolution.
Hans de Nivelle
+ Hybrid Interactive Theorem Proving using Nuprl and HOL.
Amy P. Felty, Douglas J. Howe
+ Proof Tactics for a Theory of State Machines in a Graphical Environment.
Katherine A. Eastaughffe, Maris A. Ozols, Tony Cant
+ RALL: Machine-supported Proofs for Relation Algebra.
David von Oheimb and Thomas F. Gritzner
+ Evolving Combinators.
+ Partial Matching for Analogy Discovery in Proofs and Counter-examples.
Gilles Defourneaux, Nicolas Peltier
+ DiaLog: A System for Dialogue Logic.
Jurgen Ehrensberger, Claus Zinn
+ Peers-mcd, CODE, SETHEO, KIV, SATO, Dedam, ILF, ILF-SETHEO, 3CNF, MINLOG,
PLAGIATOR, Nuprl-Light, OMEGA, XIsabelle, Snarks, XBarnacle, Jape.