[Prev][Next][Index][Thread]

CADE-14 Call for Attendance


                                   CADE-14

          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:

                    http://www.cs.jcu.edu.au/~cade-14/

 Alternatively, send us email (cade-14@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
      E-mail: cade14-chair@mcs.anl.gov  E-mail: cade-14@cs.jcu.edu.au

-------------------------------------------------------------------------------

                      CADE-14 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 Wen-Tsun, 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 Nelson-Oppen Combination Method.
  Franz Baader, Cesare Tinelli
+ On Equality Up-to 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 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.
  Uwe Egly
+ Deciding Intuitionistic Propositional  Logic via  Translation into  Classical
  Logic.
  Daniel Korn, Christoph Kreitz
+ Lemma Matching for a PTTP-based Top-down Theorem Prover.
  Koji Iwanuma
+ Exact  Knowledge Compilation in  Predicate Calculus:  the Partial Achievement
  Case.
  Olivier Roussel, Philippe Mathieu
+ Non-Horn Magic Sets to  Incorporate Top-down Inference into Bottom-up Theorem
  Proving.
  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
  Definitions.
  Sean Matthews
+ 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.
  Matthias Fuchs
+ Partial Matching for Analogy Discovery in Proofs and Counter-examples.
  Gilles Defourneaux, Nicolas Peltier
+ DiaLog: A System for Dialogue Logic.
  Jurgen Ehrensberger, Claus Zinn

System Descriptions
+ Peers-mcd,  CODE, SETHEO, KIV,  SATO, Dedam,  ILF, ILF-SETHEO, 3CNF,  MINLOG, 
  PLAGIATOR, Nuprl-Light, OMEGA, XIsabelle, Snarks, XBarnacle, Jape.

-------------------------------------------------------------------------------