🚀 go-pugleaf

From: Hans-Juergen Buerckert <buerkert@informatik.uni-kl.de>
To: mod-ki@unido.informatik.uni-dortmund.de
Date: Mon, 9 Apr 90 16:30:03 MET DST
Subject: 10th International Conference on Automated Deduction (CADE-10)
Keywords: Konferenzen

mod-ki message 0427
************************************************************************
Nachfolgend die Registrationsinfo und Tagungsprogramm der  CADE-10,  mit
der Bitte diese auszuhaengen bzw. weiterzuverteilen.
Vielen Dank Hans-Juergen Buerckert


     10th International Conference on Automated Deduction
 
                      July 24-27, 1990
 
       Registration Information and Preliminary Schedule
 
Dates
=====
 
Tutorials:                   Tuesday, July 24
Paper sessions:              Wednesday, July 25 - Friday, July 27
Early registration:          before June 15
Reservation of accomodation: before June 15
 
 
Overview
========
 
 -  Presentation of more than 40 papers on topics of
    automated deduction and related fields.
 -  Invited talks from
          Robert Boyer and J Strother Moore, Computational
          Logic Inc.: Keynote Address
          Woody Bledsoe, University of Texas: Banquet
          Address
          Wolfgang Bibel, Technische Hochschule
          Darmstadt
          Alan Bundy, University of Edinburgh
 -  Tutorials on several special areas of automated
    deduction.
 -  Reception with wine and snacks on Tuesday evening at
    the Conference hotel, Hotel DORINT.
 -  Wine tasting and dinner on Wednesday evening at one of
    the famous wine cellars of the "Suedliche Weinstrasse".
 -  Conference banquet on Thursday evening at "Hambacher
    Schloss", a famous castle, where actions of the first
    freedom and democracy movement in Germany took place in
    the middle of the last century.
 
 
Location
========
CADE-10 will be held at Kaiserslautern,  West  Germany.  The  conference
will take place at Hotel DORINT. We have reserved about 40 single and 60
double rooms in the Conference hotel. All rooms  are  with  bathroom  en
suite, radio, telephone, and colour TV. In the hotels  DORIMARE  leisure
landscape you can enjoy indoor and outdoor pools, solaria, masseurs, sun
lawn,   and   Finnish   block   hut   sauna.  There   are   the   rustic
"Betzenbergstuebchen" restaurant serving snacks and small meals and  the
"DORADO" restaurant with international  and  regional  specialities.  We
have also reserved a limited number of rooms in other hotels in the city
of Kaiserslautern. From those you can easily reach the Conference  hotel
by bus (about 15-20 minutes), by car (10 minutes),  or  by  foot  (20-30
minutes). We will try to organize a bus shuttle in the  morning  and  in
the evening between the external hotels and the Conference hotel.

Support
=======
CADE-10 is supported by
 
 -  International Joint Conference on Artificial Intelligence, Inc.
 -  Deutsche Forschungsgemeinschaft (DFG), Bonn
 -  Adam Opel AG, Werk Kaiserslautern
 -  BASF AG, Ludwigshafen
 -  Daimler Benz AG, Stuttgart
 -  Dornier GmbH, Friedrichshafen
 -  Krupp Atlas Elektronik GmbH, Bremen
 -  Siemens AG, Muenchen
 
Assistance in organizing CADE-10 was given by
 
 -  Deutsches Forschungszentrum fuer Kuenstliche
    Intelligenz (DFKI), Kaiserslautern
 -  Sonderforschungsbereich Kuenstliche Intelligenz:
    Wissensbasierte Systeme (SFB 314), Kaiserslautern
 -  Universitaet Kaiserslautern
 -  SRI International, Menlo Park, California
 -  Bell Laboratories, Murray Hill, New Jersey

Information
===========
For further information, contact
 
        Mark E. Stickel, CADE-10 Chairman
        Artificial Intelligence Center
        SRI International
        333 Ravenswood Avenue
        Menlo Park, CA 94025 USA
        Email: stickel@ai.sri.com
 
        Hans Juergen Ohlbach, CADE-10 Local Arrangements
        SFB 314, FB Informatik
        Universitaet Kaiserslautern
        Postfach 3049
        D-6750 Kaiserslautern, FR Germany
        Email: ohlbach@informatik.uni-kl.de
 or
        Hans-Juergen Buerckert, CADE-10 Local Arrangements
        Projektgruppe WINO
        DFKI Kaiserslautern
        Postfach 2080
        D-6750 Kaiserslautern, FR Germany
        Email: buerkert@informatik.uni-kl.de
 

Tutorials
=========
A: 8:30--11:00 High-Performance Automated Theorem Proving
   Ewing Lusk, William McCune (Argonne National Laboratory)
 
Since the early 70's, a series of automated theorem provers
have been developed at Argonne, based on relatively
straightforward algorithms but on increasingly sophisticated
data structures and implementation techniques.
Their objective has always been to find proofs of difficult
theorems: those requiring proofs containing many steps and
large terms.  As a result, the set of problems provable by
automated systems has been expanded to include a number of
previously open questions in logic and mathematics.
 
This tutorial will begin with a brief survey of the
philosophy that has guided the development of the systems at
Argonne, and proceed to a presentation of the key ideas in
the implementation of the current system, OTTER.  The
primary focus will be on data structures and algorithms
required to support large searches.  Parallel algorithms for
theorem proving will be described, based on both
distributed-memory and shared-memory models of computation,
and recent results with parallel versions of OTTER will be
presented.
 
B: 8:30--11:00 Reasoning and Representation with Concept
   Languages
   Juergen Mueller, Franz Baader, Bernhard Nebel,
   Werner Nutt (German Research Center on AI),
   Gert Smolka (IBM)
 
Logic-based concept languages have been extensively used for
representing knowledge in AI systems during the last decade.
Only recently have results been obtained that give a
complete overview of the decidability  and complexity of
inferences in most of these formalisms. This tutorial will
introduce two classes of concept description languages,
KL-ONE and Feature Logic, discuss classification algorithms,
their complexity and relation to automated theorem proving,
and consider several semantic approaches.
 
C: 8:30--11:00 (not yet determined)
 
D: 12:30--15:00 Lambda-Prolog
   Amy Felty (INRIA), Elsa Gunter (Bell Laboratories),
   Dale Miller (University of Pennsylvania),
   Frank Pfenning (Carnegie Mellon University)
 
The logic programming language Lambda-Prolog extends Prolog
by containing polymorphic types, higher-order programming,
Lambda-terms as data structures, higher-order unification,
modules, lexical scopes, abstract data types, and
implicational and universally quantified goals.  These
extensions are integrated into a single logical system
and provide Lambda-Prolog with expressive strengths not
found in Prolog.  After surveying various aspects of this
language, we shall focus on its uses in specifying proof
systems and implementing theorem provers.  In particular, we
shall discuss how the syntax and inference rules of object
logics can be represented and on how tactic-style theorem
provers can be written.  We shall also illustrate how proofs
can be built and manipulated in rather natural ways.
 
E: 12:30--15:00 Equational Unification
   Claude Kirchner (INRIA)
 
This tutorial presents unification, or equation solving in
abstract algebras. After an introduction to the problems of
the field, we present the general results on unification
theory, including the decidability and unification type of
various theories and classes of theories. Then, using a
rule-based view of the equation-solving process, we show
different aspects of the field. For Syntactic unification we
describe, in an abstract fashion, the classical algorithms
of Robinson and Martelli-Montanari.  Semantic unification
(i.e.,  equational unification) is then studied. We first
look at two examples, giving unification algorithms for
commutative and associative-commutative theories.  Then we
focus on the combination of unification algorithms and on
general equational unification. The notion of syntactic
theory, for which unification algorithms can be
automatically computed, is also introduced and its
usefulness shown on several examples.
 
F: 12:30--15:00 Compilation Techniques for Logics
   Hans Juergen Ohlbach (University of Kaiserslautern),
   Andreas Herzig (Universite Paul Sabatier, Toulouse)
 
Nonclassical logics, modal logics, epistemic logics,
temporal logics, action logics, etc., are becoming more and
more important for general AI applications. Recently a new
method for designing deduction calculi for such logics has
been developed. The idea is to translate formulae
of a nonclassical ``source logic'' into predicate logic
syntax, so that calculi and theorem provers for predicate
logic, in particular resolution calculi, become applicable.
In the tutorial we introduce the translation methods and
discuss their advantages and limitations.
 
G: 15:30--18:00 High-Performance Theorem Provers: Efficient
   Implementation and Parallelisation
   J. Schumann, R. Letz, F. Kurfess (Technical University
   of Munich)
 
This tutorial covers theoretical and implementation aspects
of theorem provers for first-order predicate logic, with the
focus on analytic calculi.  We concentrate on the connection
method and related calculi, especially the model elimination
calculus. After having presented the theoretical background,
we discuss refinements of the calculus (like regularity) as
well as extensions (like lemmata and proof schemata).
 
In a second part we discuss techniques for an efficient
implementation of model elimination. We describe in detail
the technique of using an abstract machine, which is an
extension of the Warren Abstract Machine (WAM). It serves as
the kernel for a family of sequential and parallel theorem
provers.
 
Exploiting the potential of parallelism in logic will be the
next major topic. Different kinds of parallelism in logic
are identified and classified with respect to parameters of
grain-size and independency of the parallel processes. One
kind of parallelism, OR-parallelism, is explained in detail
with the theorem prover PARTHEO. Questions concerning the
memory model, the distribution of work, the load balancing,
and the relation to similar approaches are discussed.
 
H: 15:30--18:00 Rewriting-Based Theorem Proving
   Jean-Pierre Jouannaud (LRI), Jieh Hsiang (SUNY
   Stony Brook)
 
I: 15:30--18:00 Program-Synthetic Deduction
   Richard Waldinger (SRI International)
 
Software development is an appropriate and promising
application of automated deduction. Theorem-proving
techniques are being applied to such tasks as program
synthesis (deriving a program to meet given specifications)
and program verification (proving that a given program does
meet its specifications). Deductive methods can also be
adapted to less demanding applications, such as bug
detection (discovering an input that causes a program to
malfunction) and program modification (altering a program to
reflect a change in its specifications). In this tutorial we
present deduction techniques particularly well suited to
software development applications.
 
 
Mark tutorial choices on registration form with capital
letters; do not register for tutorials given in parallel:
A, B, and C conflict with each other, as do D, E, and F, and
also G, H, and I.
 

Schedule of Papers
==================
Session 1: 8:30--10:00 Wednesday
   Keynote Address, Robert S. Boyer, J Strother Moore
 
 
Session 2: 10:30--12:00 Wednesday
   A Complete Semantic Back Chaining Proof System,
   Xumin Nie, David A. Plaisted
 
   Parallelizing the Closure Computation in Automated
   Deduction, John K. Slaney, Ewing L. Lusk
 
   PARTHEO: A High Performance Parallel Theorem Prover,
   J. Schumann, R. Letz

Session 3: 13:30--15:30 Wednesday
   Substitution-based Compilation of Extended Rules in
   Deductive Databases, Sang Ho Lee, Lawrence J. Henschen
 
   Automatic Theorem Proving in Paraconsistent Logics:
   Theory and Implementation, Newton C. A. da Costa,
   Lawrence J. Henschen, James J. Lu, V. S. Subrahmanian
 
   Case-Free Programs: An Abstraction of Definite Horn
   Programs, Toshiro Wakayama, T. H. Paine
 
   Generalized Well-founded Semantics for Logic Programs,
   Chitta Baral, Jorge Lobo, Jack Minker

Session 4: 13:30--15:30 Wednesday
   Tactical Theorem Proving in Program Verification,
   M. Heisel, W. Reif, W. Stephan
 
   Extensions to the Rippling-Out Tactic for Guiding
   Inductive Proofs, Alan Bundy, Frank van Harmelen,
   Alan Smaill
 
   Guiding Induction Proofs, Dieter Hutter
 
   Term Rewriting Induction, Uday S. Reddy

Session 5: 16:00--17:30 Wednesday
   A Resolution Principle for Clauses with Constraints,
   Hans-Juergen Buerckert
 
   Str+ve: The Str+ve-based Subset Prover, Larry Hines
 
   Ritt-Wu's Decomposition Algorithm and Geometry Theorem
   Proving, Shang-Ching Chou, Xiao-Shan Gao

Session 6: 8:30--10:00 Thursday
   Encoding a Dependent-Type Lambda-Calculus in a Logic
   Programming Language, Amy Felty, Dale Miller
 
   Investigations into Proof-Search in a System of First
   Order Dependent Function Types, David Pym,
   Lincoln Wallen
 
   Equality of Terms Containing Associative-Commutative
   Functions and Commutative Binding Operators is
   Isomorphism Complete, David A. Basin

Session 7: 10:30--12:00 Thursday
   An Improved General E-Unification Method,
   Daniel J. Dougherty, Patricia Johann
 
   Some Results on Equational Unification,
   Paliath Narendran, Friedrich Otto
 
   Unification in a Combination of Equational Theories:
   an Efficient Algorithm, Alexandre Boudet

Session 8: 13:30--15:30 Thursday
   SLIM: An Automated Reasoner for Equivalences, Applied
   to Set Theory, Alan F. McMichael
 
   Developing the Prolog Technology Theorem-Prover,
   Mark Tarver
 
   Presenting Intuitive Deductions via Symmetric
   Simplification, Frank Pfenning, Dan Nesmith
 
   Toward Mechanical Methods for Streamlining Proofs,
   William Pierce

Session 9: 13:30--15:30 Thursday
   Ordered Rewriting and Confluence,
   Ursula Martin, Tobias Nipkow
 
   Complete Sets of Reductions with Constraints,
   Gerald E. Peterson
 
   Rewrite Systems for Varieties of Semigroups,
   Franz Baader
 
   Improving Associative Path Orderings,
   Joachim Steinbach

Session 10: 16:00--17:00 Thursday
   Invited Talk, Wolfgang Bibel

Session 11: 8:30--10:00 Friday
   On Restrictions of Ordered Paramodulation with
   Simplification, Leo Bachmair, Harald Ganzinger
 
   Simultaneous Paramodulation, Dan Benanav
 
   Hyper Resolution and Equality Axioms without Function
   Substitutions, Lawrence Henschen, Yusuf Ozturk

Session 12: 10:30--12:00 Friday
   Automatic Acquisition of Search Guiding Heuristics,
   Christian B. Suttner, Wolfgang Ertel
 
   Automated Reasoning Contributes to Mathematics and Logic,
   L. Wos, S. Winker, W. McCune, R. Overbeek, E. Lusk,
   R. Stevens
 
   A Mechanically Assisted Constructive Proof in Category
   Theory, James A. Altucher, Prakash Panangaden

Session 13: 13:30--15:30 Friday
   Dynamic Logic as a Uniform Framework for Theorem Proving
   in Intensional Logic, Heikki Tuominen
 
   A Tableaux-Based Theorem Prover for a Decidable Subset of
   Default Logic, Camilla B. Schwind
 
   Computing Prime Implicants, Peter Jackson, John Pais
 
   Minimizing the Number of Clauses by Renaming,
   Thierry Boy de la Tour

Session 14: 13:30--15:30 Friday
   Higher Order E-Unification, Wayne Snyder
 
   Programming by Example and Proving by Example Using
   Higher-order Unification, Masami Hagiya
 
   Retrieving Library Identifiers Whose Types Are at Least
   as General, Modulo CCC-Isomorphism, as a Given Type,
   Mikael Rittri
 
   Unification in Monoidal Theories, Werner Nutt

Session 15: 16:00--17:00 Friday
   Invited Talk, Alan Bundy

------------------------------------------------------------------------
                 Registration Form
               (please print or type)
 
Please send this registration form together with your
registration fee and hotel reservation to
 
          Petra Stoll CADE-10
          DFKI, Projectgroup WINO
          Postfach 2080
          D-6750 Kaiserslautern
          FR Germany
 
You will get an affirmation and travel information etc. in
the beginning of July.
 
Name   _____________________________________________________
       (First)     (Middle)     (Last)
 
Organization   _____________________________________________
 
Business       _____________________________________________
Address
               _____________________________________________
 
               _____________________________________________
 
Electronic mail_____________________________________________
 
 
Registration Fees
=================
                           Nonstudent     Student
   Registration (early)*   DM 300.- __    DM 180.- __
     (before June 15th)
   Registration (late)     DM 350.- __    DM 250.- __
      (after June 15th)
   Wine Tasting**          DM  30.- __    DM  30.- __
      (first 100 registrations)
   Banquet Dinner**        DM  50.- __    DM  50.- __
      (first 120 registrations)
   Tutorials        one    DM 100.- __    DM  60.- __
 
                    two    DM 150.- __    DM  80.- __
 
                    three  DM 180.- __    DM 100.- __
 
Registrants may take guests to the wine tasting and banquet.
 
   Wine Tasting**   ___ guests at DM  60.- each = DM ___
   Banquet**        ___ guests at DM 100.- each = DM ___
 
Mark the letters of the tutorials you want to attend
                    ___  ___  ___
 
Total enclosed:     DM ___________________ No credit cards
 
Checks (DM only) must be made
payable to CADE-10, H.-J. Buerckert.
 
*)   This form together with fee must be at Kaiserslautern
     before June 15th for early registration.
**)  There is only a limited number of places for wine
     tasting (100) and for banquet dinner (120)
 
Housing
=======
The conference will take place at Hotel DORINT. We have  reserved  about
40 single and 60 double rooms in the Conference hotel and in addition  a
limited number of rooms in three categories in some  other  hotels.  The
number of rooms are limited. Please, book accommodation  no  later  than
June 15th; we cannot guarantee a room if your reservation arrives  after
that. Rooms are reserved on guaranteed basis. If you have  a  change  in
plans, please, advice us to cancel your reservation as soon as possible.
 
I need accommodation from _________ to _________ (__nights)
     for __ persons.
 
__  I want to share a double room with _____________________
__  I want to share a double room with someone assigned
        I am   __ male   __ female.
 
I prefer to be booked for (mark 1 for first choice, 2 for
second choice):
 
  __  the Conference Hotel (Hotel DORINT):
      __  single room (DM 128.- per night)
      __  double room (DM 185.- per night)
 
 
  __  hotel category A (bathroom, shower & toilet):
      __  single room (DM 60-80.- per night)
      __  double room (DM 90-130.- per night)
 
  __  hotel category B (bathroom, shower):
      __  single room (DM 40-65.- per night)
      __  double room (DM 70-125.- per night)
 
  __  hotel category C (no shower, no toilet):
      __  single room (DM 30-40.- per night)
      __  double room (DM 60-70.- per night)
 
  __  No housing accommodation requested***

Room prices include breakfast. The conference  hotel  also  includes  an
organized conference lunch each day.  Registrants  not  staying  at  the
conference hotel can be served at the  organized  conference  lunch  for
DM 30.- per day

If not staying at the conference hotel,
  __ I want to attend organized lunch each day
  __ I do not want to attend the conference lunch.

 
Remarks:  __________________________________________________
 
          __________________________________________________
 
          __________________________________________________
 

************************************************************************