[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