[Prev][Next][Index][Thread]
CADE14 Early Registration

To: deduktion@intellektik.informatik.thdarmstadt.de (German Deduction Group Research), theoremprovers@ai.mit.edu (MIT AI list Research), igpl@doc.ic.ac.uk (Interest Group on Propositional and Predicate Logics Research), types@dcs.gla.ac.uk (Types mailing list Research), logic@cs.stanford.edu (Stanford Logic Research), aal@anu.edu.au (Australiasian Association for Logic Research), rewriting@loria.fr (Rewriting Research), qed@mcs.anl.gov (QED Research), fg121@bach.informatik.uniulm.de (German Group Research)

Subject: CADE14 Early Registration

From: Geoff Sutcliffe <geoff@cs.jcu.edu.au>

Date: Wed, 30 Apr 1997 08:42:33 +1000 (EST)

DeliveryDate: Tue, 29 Apr 1997 17:44:55 0500
CADE14
The 14th International Conference on Automated Deduction
July 1317, 1997, Townsville, Australia
******************* EARLY REGISTRATION CLOSES ON 12 MAY ********************
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 metalogics. 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, humancomputer
R. Letz (Munich) interfaces, distributed deduction, and search
E. Lusk (Argonne) heuristics.
U. Martin (St. Andrews)
D. McAllester (Murray Hill) CADE14 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. CADE14 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 (14th17th July)
A. Voronkov (Uppsala) + Seventeen system descriptions (14th17th July)
L. Wallen (Oxford) + An ATP system competition (16th July)
C. Walther (Darmstadt) + A banquet on Magnetic Island (16th July)
D. Wang (Grenoble) + An excursion to the Great Barrier Reef
H. Zhang (Iowa City) (18th July)
You are invited to attend CADE14, to participate
in the high quality technical program, and to
enjoy some great social events.
Information and Registration
Full details about CADE14 and an electronic registration form are on the WWW:
http://www.cs.jcu.edu.au/~cade14/
Alternatively, send us email (cade14@cs.jcu.edu.au) 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
Email: cade14chair@mcs.anl.gov Email: cade14@cs.jcu.edu.au

CADE14 Advance Program Summary
Workshops
+ 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
Tutorials
+ Learning from Previous Proof Experience
+ Deduction Methods Based on Boolean Rings
+ Term Indexing in Automated Reasoning, Databases and Declarative Programming
Languages
+ Higher Order Equational Logic
Invited Lectures
+ Professor Wu WenTsun, Academia Sinica, Beijing, China
+ Professor Moshe Vardi, Rice University, Houston, USA
Research Papers
+ 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 NelsonOppen Combination Method.
Franz Baader, Cesare Tinelli
+ On Equality Upto Constraints over Finite Trees, Context Unification and One
Step Rewriting.
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.
Johann Schumann
+ A Practical Integration of FirstOrder Reasoning and Decision Procedures.
Nikolaj S. Bjorner, Mark E. Stickel and Tomas E. Uribe
+ Some Pitfalls of LKtoLJ Transformations and How to Avoid Them.
Uwe Egly
+ Deciding Intuitionistic Propositional Logic via Translation into Classical
Logic.
Daniel Korn, Christoph Kreitz
+ Lemma Matching for a PTTPbased Topdown Theorem Prover.
Koji Iwanuma
+ Exact Knowledge Compilation in Predicate Calculus: the Partial Achievement
Case.
Olivier Roussel, Philippe Mathieu
+ NonHorn Magic Sets to Incorporate Topdown Inference into Bottomup Theorem
Proving.
Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta and Miyuki Koshimura
+ ConnectionBased Proof Construction in Linear Logic.
Christoph Kreitz, Heiko Mantel, Jens Otten, Stephan Schmitt
+ Resourcedistribution 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 lambdaCalculus.
Dieter Hutter, Michael Kohlhase
+ A Practical Implementation of Simple Consequence Relations Using Inductive
Definitions.
Sean Matthews
+ Soft Typing for Ordered Resolution.
Harald Ganzinger, Christoph Meyer, Christoph Weidenbach
+ A Classification of NonLiftable 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: Machinesupported Proofs for Relation Algebra.
David von Oheimb and Thomas F. Gritzner
+ Evolving Combinators.
Matthias Fuchs
+ Partial Matching for Analogy Discovery in Proofs and Counterexamples.
Gilles Defourneaux, Nicolas Peltier
+ DiaLog: A System for Dialogue Logic.
Jurgen Ehrensberger, Claus Zinn
System Descriptions
+ Peersmcd, CODE, SETHEO, KIV, SATO, Dedam, ILF, ILFSETHEO, 3CNF, MINLOG,
PLAGIATOR, NuprlLight, OMEGA, XIsabelle, Snarks, XBarnacle, Jape.
