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

CADE-11



Date: Wed, 8 Apr 92 01:30:09 -0400

                    CADE-11   General Information

        The Eleventh International Conference on Automated  Deduc-
   tion  will  be held at the Ramada Renaissance Hotel in Saratoga
   Springs, NY and will be hosted by the State University  of  New
   York  at  Albany.   Forms  for conference registration and room
   reservations, brochures and maps  providing  information  about
   local  hotels/motels  and  restaurants,  a  preliminary program
   listing, and the conference poster are being sent  via  regular
   mail.

        The conference will begin with a welcome reception at  the
   Ramada  Renaissance  Hotel on Sunday, June 14, 7:00pm - 9:00pm.
   The tutorials will  take  place  on  Monday,  June  15.   Paper
   presentations  will  occur Tues. - Thurs., 6/16-18.  During the
   conference, several workstations will be available for  demons-
   tration of working systems.

        The conference banquet will be held on Tuesday evening and
   will  feature  Ray  Smullyan as the speaker.  For Wednesday, an
   excursion dinner is planned on board the Lac  du  Saint  Sacre-
   ment,  which  will  sail  the  southern basin of beautiful Lake
   George.

        More  specific  information  on  travel,   accommodations,
   conference tutorials and events, and system demonstration capa-
   bilities, is outlined below.

   TRAVEL  INFORMATION

        Special rates for CADE-11 attendees are being  offered  by
   Delta  Air  Lines,  Inc.   A  40% reduction on applicable coach
   fares can be obtained if tickets are purchased at least 7  days
   prior  to  departure.  These tickets are sold on a limited seat
   basis, but are fully refundable.  Except for Canadian  origina-
   tions,  a  5%  discount  is offered on promotional fares (e.g.,
   super-saver fares).  To obtain these  discounts,  you  or  your
   travel  agent  should  call  1-800-221-1212,  and refer to file
   reference G32069.

        Saratoga Springs is 25 miles north of the  Albany  airport
   just off Interstate I87.  For those planning to rent a car, the
   drive is very easy, about 25 min. (We  suggest  driving  at  or
   below 65 mph; I87 is heavily patroled by NYS Police.)

        Average taxi fare from the airport to  Saratoga  is  about
   $30.   However,  attendees  may  call Central Taxi (346-2344 or
   346-1231), identify themselves  as  CADE-11  participants,  and
   obtain  a  single person rate of around $25.  If several atten-
   dees are requesting transportation at the same time,  the  cost
   per  person  will decrease; depending on demand, vans or busses
   will be dispatched to provide service, and  the  cost  will  be



                            April 5, 1992





                                - 2 -


   lower  still.   Similar arrangements will be employed for those
   returning to the airport from Saratoga after the conference.

        Other options include  bus  (Trailways)  connections  from
   downtown   Albany,  and  train  (Amtrak)  connections  via  the
   Albany-Rensselaer Station and via Penn Station in NY  City,  to
   Saratoga.

   ACCOMMODATIONS

        Room blocks are being held by the Ramada, Holiday Inn, and
   Rip Van Dam motels. Rates start at $75, $58, and $40, for these
   motels, respectively.  All three are  on  Broadway,  Saratoga's
   main road.  The Ramada is next to the City Center; the  Holiday
   Inn is at Broadway and  Circular;  the  Rip  Van  Dam  is  near
   Broadway and Washington St.  The latter two motels are about 12
   and 7 minutes walking distance from the  Ramada,  respectively.
   The brochures (and map)  we  are  sending  will  give  you  the
   approximate location of these motels and  information  on  many
   others.

        Room reservation forms should be mailed  directly  to  the
   motel  at which the reservation is requested.  All three motels
   require one night's deposit.  Personal checks in  U.S.  dollars
   or  credit  card  numbers may be supplied; Holiday Inn reserva-
   tions may also be made by calling 1-800-HOLIDAY and giving  the
   three-letter  code  "CAD." Note that reservation deadlines vary
   somewhat among the motels; see the enclosed forms for details.

   CONFERENCE  EVENTS

        The registration fee is  $250  before  May  15,  and  $275
  afterwards.  Students may register for $100.

        The conference banquet will be held at the Hall of Springs
   on  Tuesday  night,  June  16. Ray Smullyan will be the banquet
   speaker; his talk is entitled ``Puzzles  and  Paradoxes.''  The
   banquet  is  free  for  conference  attendees and costs $25 for
   additional guests.

        On Wednesday night an excursion dinner cruise is  planned.
   We have chartered Lake George's largest (capacity of up to 1000
   passengers) and newest cruise ship, the Lac du Saint Sacrement.
   Lake  George  is one of America's most famous lakes. It is from
   one to four miles wide, about 32 miles long, and  is  virtually
   surrounded  by  small  mountains.   Even  today, its waters are
   clear enough that objects can be observed at a depth of 20 feet
   on  sunny  days.   The excursion is $25 for those registered at
   the conference, $50 for additional guests.

        Busses will be provided for transport to and from both the
   banquet and the excursion.

   SYSTEM  DEMONSTRATIONS

        We will have a  room  dedicated  to  software  demos;  SUN
   Microsystems,  Inc.  is  lending  five workstations for our use
   (SPARC-2, IPX, and IPC).  The installed operating  system  will
   be  SUN  OS 4.1 (or greater).  The machines will be stand-alone



                            April 5, 1992





                                - 3 -


   with local disk, @quarter@-inch tape cassette, and at least 16M
   of RAM.

        If you would like to use these facilities to demonstrate a
   working  system, please contact the Local Arrangements Chair at
   the conference address via regular or  e-mail.   Sorry  -  demo
   systems  must  be  brought  on  tape;  we will not be receiving
   software over the net.  Those exhibiting systems built on LISP,
   Prolog,  or  another  language are advised to bring and install
   what they need, when in doubt.

   CONFERENCE  TUTORIALS

        Five tutorials will be held on Monday, June 15; the fee is
   $40. for each tutorial attended (maximum of three).



                            April 5, 1992





                                - 4 -



                   CADE - 11   Preliminary  Program


                            Sunday, June 14
                Reception:  7:00pm (Renaissance Ramada)
                            Monday, June 15


                              Tutorial 1
                    Peter Andrews & Frank Pfenning
                           9:00am - 11:30am
                        TUTORIAL ON TYPE THEORY


        This tutorial will provide  a  basic  introduction  to  type
   theory,  with  emphasis on formulations employing typed @lambda@-
   calculi.  Both classical and constructive  type  theories,  which
   provide foundations for mathematics and computer science, will be
   covered.

                              Tutorial 2
                       John Slaney & Ewing Lusk
                           9:00am - 11:30am
              Finding Models: Techniques and Applications

        This tutorial is in  three  parts.  In  the  first  part  we
   describe  some  backtracking search methods for generating models
   of first order theories.  Secondly, we describe the use of  back-
   tracking  search  as a style of reasoning suitable for some kinds
   of problem solving.  Finally, we discuss model finding as part of
   an automated deduction system.


                              Tutorial 3
                             Edmund Clarke
                            1:00pm - 3:30pm
       Symbolic Model Checking - @10 sup 130@ States and Beyond

        In this tutorial we will describe the theoretical basis  for
   Symbolic Model Checking and discuss how it has been used to veri-
   fy some realistic examples.  If facilities are available we  will
   also demonstrate the use of the verifier.


                              Tutorial 4
                Helene Kirchner and Michael Rusinowitch
                       Term Rewriting Techniques


        This tutorial is an attempt to give a progressive and  homo-
   geneous   presentation  of  applications  of  term  rewriting  to
   automated theorem proving.  Theorem proving methods are presented
   using  a  common  formalism  of  inference rules to emphasize the



                            April 5, 1992





                                - 5 -


   connections and common features among the different theorem prov-
   ing systems.

                              Tutorial 5
                   Hubert Comon and Claude Kirchner
                            4:00pm - 6:30pm
                         Constraints on Trees


        This tutorial presents several constraint systems, i.e. for-
   mulae  together  with  a semantic domain and a constraint solving
   technique; we consider  only  interpretations  in  term  algebras
   T(F,X)  or  T(F,X)/(=E).  These kinds of constraints are particu-
   larly useful in automated deduction with constraints and in logic
   programming with constraints, in particular for reducing the com-
   plexity of computations and expressing strategies.


                            April 5, 1992





                                - 6 -


                          Tuesday,  June  16
                     Session I    9:30am - 10:30am
                    Larry Wos       Keynote Adress
                          Award Presentation

                       Break   10:30am - 11:00am


   Session II    11:00am - 12:30pm


   Kurt Ammon
   Automatic Proofs in Mathematical Logic and Analysis

   Shang-Ching Chou and Xiao-Shan Gao
   Proving Geometry Statements of Constructive Type

   L.M. Hines
   The Central Variable Strategy of Str+ve

                        Lunch   12:30pm - 1:30pm


   Session  III A    1:30pm - 3:30pm


   Franz Baader and Klaus U. Schulz
   Unification in the Union of Disjoint Equational Theories: Com-
   bining Decision Procedures

   Tobias Nipkow and Zhenyu Qian
   Reduction and Unification in Lambda Calculi with Subtypes

   Daniel J. Dougherty and Patricia Johann
   A Combinatory Logic Approach to Higher-Order  E-Unification

                            "              "    "
   Wolfgang Bibel, Steffen Holldobler and Jorg Wurtz
   Cycle Unification



   Session  III B    1:30pm - 3:30pm


   Katherine A. Yelick and Stephen J. Garland
   A Parallel Completion Procedure for Term Rewriting Systems

   David McAllester
   Grammar Rewriting

   Adam Cichon and Pierre Lescanne
   Polynomial Interpretations and the Complexity of Algorithms

   Leonidas Fegaras, Tim Sheard and David Stemple
   Uniform Traversal Combinators: Definition, Use and Properties



   Session  IV    4:00pm - 5:30pm

      ,
   Tomas E. Uribe
   Sorted Unification Using Set Constraints

   Alan M. Frisch and Anthony G. Cohn
   An Abstract View of Sorted Unification

   Alexandre Boudet
   Unification in Order-Sorted Algebras with Overloading



                            April 5, 1992





                                - 7 -


   Session  V    Banquet Address:  Raymond Smullyan, ``Puzzles and Paradoxes''
              Conference Banquet   6:45pm - 9:00pm,  Hall of Springs



   Wednesday,  June  17
   Session  VI    9:00am - 10:30am


   William McCune and Larry Wos
   Experiments in Automated Deduction with Condensed Detachment

   Owen L. Astrachan and Mark E. Stickel
   Caching and Lemmaizing in Model Elimination Theorem Provers

   Vincent J. Digricoli and Eugene Kochendorfer
   LIM+ Challenge Problems by RUE Hyper-Resolution
                        Break   10:30am - 11:00am


   Session  VII   11:00am - 12:30pm


   Peter Jackson
   Computing Prime Implicates Incrementally

   Geoff Sutcliffe
   Linear-Input Subset Analysis

   Belaid Benhamou and Lakhdar Sais
   Theoretical Study of Symmetries in Propositional Calculus and
   Applications
                        Lunch   12:30pm - 1:30pm


   Session  VIII A   1:30pm - 3:30pm


   David Basin and Toby Walsh
   Difference Matching

   Jane Hesketh, Alan Bundy and Alan Smaill
   Using Middle-Out Reasoning to Control the Synthesis of Tail-
   Recursive Programs

   Toby Walsh, Alex Nunes and Alan Bundy
   The Use of Proof Plans to Sum Series

   Martin Protzen
   Disproving Conjectures

                    Session  VIII B   1:30pm - 3:30pm


   Mathias Bauer
   An Interval-based Temporal Logic in a Multivalued Setting

   Michael Fisher
   A Normal Form for First-Order Temporal Formulae
                         ,
   Ricardo Caferra and Stephane Demri
   Semantic Entailment in Non Classical Logics Based on Proofs
   Found in Classical Logic

   Katsumi Inoue, Miyuki Koshimura and Ryuzo Hasegawa
   Embedding Negation as Failure into a Model Generation Theorem
   Prover

                         Break   3:30pm - 4:00pm


                            April 5, 1992





                                - 8 -


   Session  IX   4:00pm - 5:30pm


   Robert S. Boyer and Yuan Yu
   Automated Correctness Proofs of Machine Code Programs for a
   Commercial Microprocessor

   Hantao Zhang and Xin Hua
   Proving the Chinese Remainder Theorem by the Cover Set Induc-
   tion

   Peter Madden
   Automatic Program Optimization Through Proof Transformation


              Excursion  Dinner  Cruise  on  Lake  George
          on  the   Lac du Saint Sacrement   6:30pm - 10:30pm


                               Thursday,  June  18
                 Session  X    9:00am - 10:00am    Invited  Talk:
   Grigori  Mints,   ``Proof Search Theory and Practice in the (former) USSR''

                            Break   10:30am - 11:00am


   Session  XI    10:30am - 12:30pm


   Leo Bachmair, Harald Ganzinger, Christopher Lynch and
   Wayne Snyder
   Basic Paramodulation and Superposition

   Robert Nieuwenhuis and Albert Rubio
   Theorem Proving with Ordering Constrained Clauses

   Zohar Manna and Richard Waldinger
   The Special-Relation Rules are Incomplete
                                "
   Bernhard Beckert and Reiner Hahnle
   An Improved Method for Adding Equality to Free Variable Seman-
   tic Tableaux
                        Lunch   12:30pm - 1:30pm


   Session  XII A    1:30pm - 3:30pm


   N. Shankar
   Proof Search in the Intuitionistic Sequent Calculus

   Frank Pfenning and Ekkehard Rohwedder
   Implementing the Meta-Theory of Deductive Systems

   Wilfred Z. Chen
   Tactic-based Theorem Proving and Knowledge-based Forward
   Chaining: An Experiment with Nuprl and Ontic

   William M. Farmer, Joshua D. Guttman and F. Javier Thayer
   Little Theories


                            April 5, 1992





                                - 9 -


   Session  XII B    1:30pm - 3:30pm


   Jim Christian
   Some Termination Criteria for Narrowing and E-narrowing

   Nachum Dershowitz, Subrata Mitra and G. Sivakumar
   Decidable Matching for Convergent Systems

   Delia Kesner
   Free Sequentiality in Orthogonal Order-Sorted Rewriting Sys-
   tems with Constructors

   R.C. Sekar and I.V. Ramakrishnan
   Programming with Equations: A Framework for Lazy Parallel
   Evaluation

                         Break   3:30pm - 4:00pm


   Session  XIII    4:00pm - 5:30pm

   Anthony G. Cohn
   A Many Sorted Logic with Possibly Empty Sorts

   Andrei Voronkov
   Theorem Proving in Non-Standard Logics Based on the Inverse
   Method

   Konstantine Vershinin and Igor Romanenko
   One More Logic with Uncertainty and Resolution Principle for
   It



   System  Abstracts


   Li Dafa
   A Natural Deduction Automated Theorem Proving System

   Tobias Nipkow and Lawrence Paulson
   Isabelle-91

   Geoff Sutcliffe
   The Semantically Guided Linear Deduction System

   Kurt Ammon
   The SHUNYATA System

   Shang-Ching Chou
   A Geometry Theorem Prover for Macintoshes



                            April 5, 1992





                               - 10 -




   Xin Hua and Hantao Zhang
   FRI: Failure-Resistant Induction in RRL

   Hantao Zhang
   Herky: High Performance Rewriting in RRL

   William M. Farmer, Joshua D. Guttman and F. Javier Thayer
   IMPS: System Description

   Geoffrey D. Alexander and David A. Plaisted
   Proving Equality Theorems with Hyper-Linking

   Jawahar Chirimar, Carl A. Gunter and Myra VanInwegen
   Xpnet: A Graphical Interface to Proof Nets with an Efficient
   Proof Checker

   Dave Barker-Plummer, Sidney C. Bailin and Andrew S. Merrill
   &: Automated Natural Deduction

      ,
   Tomas E. Uribe, Alan M. Frisch and Michael K.chell
   An Overview of FRAPPS 2.0: A Framework for Resolution-Based
   Automated Proof Procedure Systems

   Dave Barker-Plummer, Alex Rothenberg
   The GAZER Theorem Prover

   Ewing Lusk, William McCune and John Slaney
   ROO: A Parallel Theorem Prover

   T.C. Wang and Allen Goldberg
   RVF: An Automated Formal Verification System

   Johann M.Ph. Schumann
   KPROP - An AND-parallel Theorem Prover for Propositional Logic
   Implemented in KL1

   K. Blackburn
   A Report on ICL HOL

   S. Owre, J.M. Rushby and N. Shankar
   PVS: A Prototype Verification System

   Wolfgang Reif
   The KIV System: Systematic Construction of Verified Software

   Bernhard Beckert, Reiner Hahnle, Stefan Gerberding and
   Werner Kernig                          A
   The Tableau-Based Theorem Prover      T P   for
   Multiple-Valued Logics               3

   Edmund Clarke and Xudong Zhao
   Analytica - A Theorem Prover in Mathematica

   Klaus Schneider, Ramayya Kumar and Thomas Kropf
   The FAUST-Prover

   Dan Craigen, Sentot Kromodimoeljo, Irwin Meisels, Bill Pase
   and Mark Saaltink
   Eves System Description

   Ryuzo Hasegawa, Miyuki Koshimura and Hiroshi Fa
   MGTP: A Parallel Theorem Prover Based on Lazy Model Generation


                            April 5, 1992





                               - 11 -


   Problem  Sets


   Ewing Lusk and Larry Wos
   Benchmark Problems in which Equality Plays the Major Role

   D.A. Randell, A.G. Cohn and Z. Cui
   Computing Transitivity Tables: A Challenge for Automated
   Theorem Provers