stevens@ANL-MCS.ARPA (Rick L. Stevens) (11/04/87)
Final Call for Papers
9th International Conference on Automated
Deduction
May 23-26, 1988
CADE-9 will be held at Argonne National Laboratory (near
Chicago) in celebration of the 25th anniversary of the
discovery of the resolution principle at Argonne in the sum-
mer of 1963. Papers are invited in the following or related
fields:
Theorem Proving Logic Programming
Unification Deductive Databases
Term Rewriting ATP for Non-Standard Logics
Program Verification Inference Systems
The Program Committee consists of:
Peter Andrews Ewing Lusk
W.W. Bledsoe Michael MacRobbie
Alan Bundy Hans-Jorgen Ohlbach
Robert Constable Ross Overbeek
Seif Haridi William Pase
Larry Henschen Jorg Siekmann
Deepak Kapur Mark Stickel
Dallas Lankford Jim Williams
Jean-Louis Lassez
Papers are solicited in three categories:
Long papers: 20 pages, about 5000 words
Short papers: 10 pages, about 2500 words
Extended Abstracts of Working Systems: 2 pages
Problem sets: 5 pages
Long papers are expected to present substantial research
results. Short papers are a forum for briefer presentations
of the results of ongoing research. Extended abstracts are
descriptions of existing automated reasoning systems and
their areas of application. Problem sets should present a
complete, formal representation of some collection of
interesting problems for automated systems to attack. The
problems should currently unavailable in the existing
literature. Three copies should be sent to arrive before
November 23rd, 1987 to
Ewing Lusk and Ross Overbeek, chairmen
CADE-9
Mathematics and Computer Science Division
Argonne National Laboratory
9700 South Cass Avenue
Argonne, IL 60439
Schedule:
November 23, 1987: papers due
January 25, 1988: notification of authors
February 21, 1988: final manuscripts due
Questions should be directed to E. L. Lusk (lusk@anl-
mcs.arpa, phone 312-972-7852) or Ross Overbeek
(overbeek@anl-mcs.arpa, phone 312-972-7856)lusk@ANL-MCS.ARPA (Rusty Lusk) (02/11/88)
CADE - 9
9th International Conference on Automated Deduction
May 23-26, 1988
Preliminary Schedule and Registration Information
CADE-9 will be held at Argonne National Laboratory (near Chicago) in cele-
bration of the 25th anniversary of the discovery of the resolution princi-
ple at Argonne in the summer of 1963.
Dates
Tutorials: Monday, May 23
Conference: Tuesday, May 24 - Thursday, May 26
Main Attractions:
1. Presentation of more than sixty papers related to aspects of automated
deduction. (A detailed listing of the papers is attached.)
2. Invited talks from
Bill Miller, president, SRI International
J. A. Robinson, Syracuse University
Larry Wos, Argonne National Laboratory
all of whom were at Argonne 25 years ago when the resolution principle
was discovered.
3. Organized dinners every night, including the Conference banquet,
"Dinner with the Dinosaurs", at Chicago's Field Museum of Natural His-
tory.
4. Facilities for demonstration of and experimentation with automated
deduction systems.
5. Tutorials in a number of special areas within automated deduction.
Tutorials:
We have tried to make the tutorials relatively short and inexpensive. It
is hoped that many researchers that are skilled in specialized areas of
automated deduction will take the opportunity to get an overview of related
research areas. Some of the details (like titles, exactly which member of
a team will give the tutorial, etc.) have not yet been finalized. The fol-
lowing information reflects our current information. It may change
slightly, but expect that no major changes will occur.
Tutorial 1: Constraint Logic Programming
This will be a tutorial on the Constraint Logic Programming Scheme,
and systems that have implemented the concepts (see "Constraint Logic
Programming", J. Jaffar and J-L Lassez, Proc. POPL87, Munich, January
1987).
Tutorial 2: Verification and Synthesis
This will be a tutorial by Zohar Manna and Richard Waldinger on their
work in verification and synthesis of algorithms.
Tutorial 3: Rewrite Systems
This will be a tutorial given by Mark Stickel covering the basic ideas
of equality rewrite systems.
Tutorial 4: Theorem Proving in Non-Standard Logics
This tutorial will be given by Michael McRobbie. It will cover a
number of topics from his new book.
Tutorial 5: Implementation I: Connection Graphs
This tutorial will be given by members of the SEKI project. It will
cover issues concerning why connections graphs are used and how they
can be implemented.
Tutorial 6: Implementation II: an Argonne Perspective
This tutorial will present the central implementation issues from the
perspective of a number of members of the Argonne group. It will
cover topics like choice of language, indexing, basic algorithms, and
utilization of multiprocessors.
Tutorial 7: Open questions for Research
This tutorial will be given by Larry Wos. It will focus on two col-
lections of open questions. One set consists of questions about the
field of automated theorem proving itself, questions whose answers
will materially increase the power of theorem-proving programs. The
other set consists of questions taken from various fields of mathemat-
ics and logic, questions that one might attack with the assistance of
a theorem-proving program. Both sets of questions provide intriguing
challenges for possible research.
How to Register
Fill out the following registration form (the part of this message between
the rows of ='s) and return as soon as possible to:
Mrs. Miriam L. Holden, Director
Conference Services
Argonne National Laboratory
9700 South Cass Avenue
Argonne, IL 60439
U. S. A.
Questions relating to registration and accommodations can be directed to
Ms. Miriam Holden or Joan Brunsvold at (312) 972-5587.
[Contact the message author for registration and hotel forms and for
the schedule of sessions and social events. -- KIL]
Preliminary Session Schedule
Session 1
First-Order Theorem Proving Using Conditional Rewriting
Hantao Zhang
Deepak Kapur
Elements of Z-Module Reasoning
T.C. Wang
Session 2
Flexible Application of Generalised Solutions Using Higher Order Resolution
Michael R. Donat
Lincoln A. Wallen
Specifying Theorem Provers in a Higher-Order Logic Programming Language
Amy Felty
Dale Miller
Query Processing in Quantitative Logic Programming
V. S. Subrahmanian
Session 3
An Environment for Automated Reasoning About Partial Functions
David A. Basin
The Use of Explicit Plans to Guide Inductive Proofs
Alan Bundy
LOGICALC: an environment for interactive proof development
D. Duchier
D. McDermott
Session 4
Implementing Verification Strategies in the KIV-System
M. Heisel
W. Reif
W. Stephan
Checking Natural Language Proofs
Donald Simon
Consistency of Rule-based Expert Systems
Marc Bezem
Session 5
A Mechanizable Induction Principle for Equational Specifications
Hantao Zhang
Deepak Kapur
Mukkai S. Krishnamoorthy
Finding Canonical Rewriting Systems Equivalent to a Finite Set of
Ground Equations in Polynomial Time
Jean Gallier
Paliath Narendran
David Plaisted
Stan Raatz
Wayne Snyder
Session 6
Towards Efficient Knowledge-Based Automated Theorem Proving for
Non-Standard Logics
Michael A. McRobbie
Robert K. Meyer
Paul B. Thistlewaite
Propositional Temporal Interval Logic is PSPACE
A. A. Aaby
K. T. Narayana
Session 7
Computational Metatheory in Nuprl
Douglas J. Howe
Type Inference and Its Applications in Prolog
H. Azzoune
Session 8
Procedural Interpretation of Non-Horn Logic Programs
Arcot Rajasekar
Jack Minker
Recursive Query Answering with Non-Horn Clauses
Shan Chi
Lawrence J. Henschen
Session 9
Case Inference in Resolution-Based Languages
T. Wakayama
T.H. Payne
Notes on Prolog Program Transformations, Prolog Style, and Efficient
Compilation to the Warren Abstract Machine
Ralph M. Butler
Rasiah Loganantharaj
Exploitation of Parallelism in Prototypical Deduction Problems
Ralph M. Butler
Nicholas T. Karonis
Session 10
A Decision Procedure for Unquantified Formulas of Graph Theory
Louise E. Moser
Adventures in Associative-Commutative Unification (A Summary)
Patrick Lincoln
Jim Christian
Unification in Finite Algebras is Unitary(?)
Wolfram Buttner
Session 11
Unification in a Combination of Arbitrary Disjoint Equational Theories
Manfred Schmidt-Schauss
Partial Unification for Graph Based Equational Reasoning
Karl Hans Blasius
Jorg Siekmann
Session 12
SATCHMO: A theorem prover implemented in Prolog
Rainer Manthey
Francois Bry
Term Rewriting: Some Experimental Results
Richard C. Potter
David Plaisted
Session 13
Analogical Reasoning and Proof Discovery
Bishop Brock
Shaun Cooper
William Pierce
Hyper-Chaining and Knowledge-Based Theorem Proving
Larry Hines
Session 14
Linear Modal Deductions
L. Farinas del Cerro
A. Herzig
A Resolution Calculus for Modal Logics
Hans Jurgen Ohlbach
Session 15
Solving Disequations in Equational Theories
Hans-Jurgen Burckert
On Word Problems in Horn Theories
Emmanuel Kounalis
Michael Rusinowitch
Canonical Conditional Rewrite Systems
Nachum Dershowitz
Mitsuhiro Okada
G. Sivakumar
Program Synthesis by Completion with Dependent Subtypes
Paul Jacquet
Session 16
Reasoning about Systems of Linear Inequalities
Thomas Kaufl
A Subsumption Algorithm Based on Characteristic Matrices
Rolf Socher
A Restriction of Factoring in Binary Resolution
Arkady Rabinov
Supposition-Based Logic for Automated Nonmonotonic Reasoning
Philippe Besnard
Pierre Siegal
Session 17
Argument-Bounded Algorithms as a Basis for Automated Termination Proofs
Christoph Walther
Automated Aids in Implementation Proofs
Leo Marcus
Timothy Redmond
Session 18
A New Approach to Universal Unification and Its Application to AC-Unification
Mark Franzen
Lawrence J. Henschen
An Implementation of a Dissolution-Based System Employing Theory Links
Neil V. Murray
Erik Rosenthal
Session 19
Decision Procedure for Autoepistemic Logic
Ilkka Niemela
Logical Matrix Generation and Testing
Peter K. Malkin
Errol P. Martin
Optimal Time Parallel Algorithms for Term Matching
Rakesh M. Verma
I.V. Ramakrishnan
Session 20
Challenge Equality Problems in Lattice Theory
William McCune
Single Axioms in the Implicational Propositional Calculus
Frank Pfenning
Challenge Problems Focusing on Equality and Combinatory Logic:
Evaluating Automated Theorem-Proving Programs
Larry Wos
William McCune
Challenge Problems from Nonassociative Rings for Theorem Provers
Rick Stevensstevens%antares@ANL-MCS.ARPA (04/15/88)
CADE - 9
9th International Conference on Automated Deduction
May 23-26, 1988
Preliminary Schedule and Registration Information
CADE-9 will be held at Argonne National Laboratory (near Chicago) in cele-
bration of the 25th anniversary of the discovery of the resolution princi-
ple at Argonne in the summer of 1963.
Dates
Tutorials: Monday, May 23
Conference: Tuesday, May 24 - Thursday, May 26
Main Attractions:
1. Presentation of more than sixty papers related to aspects of automated
deduction. (A detailed listing of the papers is attached.)
2. Invited talks from
Bill Miller, president, SRI International
J. A. Robinson, Syracuse University
Larry Wos, Argonne National Laboratory
all of whom were at Argonne 25 years ago when the resolution principle
was discovered.
3. Organized dinners every night, including the Conference banquet,
"Dinner with the Dinosaurs", at Chicago's Field Museum of Natural His-
tory.
4. Facilities for demonstration of and experimentation with automated
deduction systems.
5. Tutorials in a number of special areas within automated deduction.
Tutorials:
We have tried to make the tutorials relatively short and inexpensive. It
is hoped that many researchers that are skilled in specialized areas of
automated deduction will take the opportunity to get an overview of related
research areas. Some of the details (like titles, exactly which member of
a team will give the tutorial, etc.) have not yet been finalized. The fol-
lowing information reflects our current information. It may change
slightly, but expect that no major changes will occur.
Tutorial 1: Constraint Logic Programming
This will be a tutorial on the Constraint Logic Programming Scheme,
and systems that have implemented the concepts (see "Constraint Logic
Programming", J. Jaffar and J-L Lassez, Proc. POPL87, Munich, January
1987).
Tutorial 2: Verification and Synthesis
This will be a tutorial by Zohar Manna and Richard Waldinger on their
work in verification and synthesis of algorithms.
Tutorial 3: Rewrite Systems
This will be a tutorial given by Mark Stickel covering the basic ideas
of equality rewrite systems.
Tutorial 4: Theorem Proving in Non-Standard Logics
This tutorial will be given by Michael McRobbie. It will cover a
number of topics from his new book.
Tutorial 5: Implementation I: Connection Graphs
This tutorial will be given by members of the SEKI project. It will
cover issues concerning why connections graphs are used and how they
can be implemented.
Tutorial 6: Implementation II: an Argonne Perspective
This tutorial will present the central implementation issues from the
perspective of a number of members of the Argonne group. It will
cover topics like choice of language, indexing, basic algorithms, and
utilization of multiprocessors.
Tutorial 7: Open questions for Research
This tutorial will be given by Larry Wos. It will focus on two col-
lections of open questions. One set consists of questions about the
field of automated theorem proving itself, questions whose answers
will materially increase the power of theorem-proving programs. The
other set consists of questions taken from various fields of mathemat-
ics and logic, questions that one might attack with the assistance of
a theorem-proving program. Both sets of questions provide intriguing
challenges for possible research.
How to Register
Fill out the following registration form (the part of this message between
the rows of ='s) and return as soon as possible to:
Mrs. Miriam L. Holden, Director
Conference Services
Argonne National Laboratory
9700 South Cass Avenue
Argonne, IL 60439
U. S. A.
Questions relating to registration and accommodations can be directed to
Ms. Miriam Holden or Joan Brunsvold at (312) 972-5587.
[...]
Session Schedule
Session 1
First-Order Theorem Proving Using Conditional Rewriting
Hantao Zhang
Deepak Kapur
Elements of Z-Module Reasoning
T.C. Wang
Session 2
Flexible Application of Generalised Solutions Using Higher Order Resolution
Michael R. Donat
Lincoln A. Wallen
Specifying Theorem Provers in a Higher-Order Logic Programming Language
Amy Felty
Dale Miller
Query Processing in Quantitative Logic Programming
V. S. Subrahmanian
Session 3
An Environment for Automated Reasoning About Partial Functions
David A. Basin
The Use of Explicit Plans to Guide Inductive Proofs
Alan Bundy
LOGICALC: an environment for interactive proof development
D. Duchier
D. McDermott
Session 4
Implementing Verification Strategies in the KIV-System
M. Heisel
W. Reif
W. Stephan
Checking Natural Language Proofs
Donald Simon
Consistency of Rule-based Expert Systems
Marc Bezem
Session 5
A Mechanizable Induction Principle for Equational Specifications
Hantao Zhang
Deepak Kapur
Mukkai S. Krishnamoorthy
Finding Canonical Rewriting Systems Equivalent to a Finite Set of
Ground Equations in Polynomial Time
Jean Gallier
Paliath Narendran
David Plaisted
Stan Raatz
Wayne Snyder
Session 6
Towards Efficient Knowledge-Based Automated Theorem Proving for
Non-Standard Logics
Michael A. McRobbie
Robert K. Meyer
Paul B. Thistlewaite
Propositional Temporal Interval Logic is PSPACE
A. A. Aaby
K. T. Narayana
Session 7
Computational Metatheory in Nuprl
Douglas J. Howe
Type Inference and Its Applications in Prolog
H. Azzoune
Session 8
Procedural Interpretation of Non-Horn Logic Programs
Arcot Rajasekar
Jack Minker
Recursive Query Answering with Non-Horn Clauses
Shan Chi
Lawrence J. Henschen
Session 9
Case Inference in Resolution-Based Languages
T. Wakayama
T.H. Payne
Notes on Prolog Program Transformations, Prolog Style, and Efficient
Compilation to the Warren Abstract Machine
Ralph M. Butler
Rasiah Loganantharaj
Exploitation of Parallelism in Prototypical Deduction Problems
Ralph M. Butler
Nicholas T. Karonis
Session 10
A Decision Procedure for Unquantified Formulas of Graph Theory
Louise E. Moser
Adventures in Associative-Commutative Unification (A Summary)
Patrick Lincoln
Jim Christian
Unification in Finite Algebras is Unitary(?)
Wolfram Buttner
Session 11
Unification in a Combination of Arbitrary Disjoint Equational Theories
Manfred Schmidt-Schauss
Partial Unification for Graph Based Equational Reasoning
Karl Hans Blasius
Jorg Siekmann
Session 12
SATCHMO: A theorem prover implemented in Prolog
Rainer Manthey
Francois Bry
Term Rewriting: Some Experimental Results
Richard C. Potter
David Plaisted
Session 13
Analogical Reasoning and Proof Discovery
Bishop Brock
Shaun Cooper
William Pierce
Hyper-Chaining and Knowledge-Based Theorem Proving
Larry Hines
Session 14
Linear Modal Deductions
L. Farinas del Cerro
A. Herzig
A Resolution Calculus for Modal Logics
Hans Jurgen Ohlbach
Session 15
Solving Disequations in Equational Theories
Hans-Jurgen Burckert
On Word Problems in Horn Theories
Emmanuel Kounalis
Michael Rusinowitch
Canonical Conditional Rewrite Systems
Nachum Dershowitz
Mitsuhiro Okada
G. Sivakumar
Program Synthesis by Completion with Dependent Subtypes
Paul Jacquet
Session 16
Reasoning about Systems of Linear Inequalities
Thomas Kaufl
A Subsumption Algorithm Based on Characteristic Matrices
Rolf Socher
A Restriction of Factoring in Binary Resolution
Arkady Rabinov
Supposition-Based Logic for Automated Nonmonotonic Reasoning
Philippe Besnard
Pierre Siegal
Session 17
Argument-Bounded Algorithms as a Basis for Automated Termination Proofs
Christoph Walther
Automated Aids in Implementation Proofs
Leo Marcus
Timothy Redmond
Session 18
A New Approach to Universal Unification and Its Application to AC-Unification
Mark Franzen
Lawrence J. Henschen
An Implementation of a Dissolution-Based System Employing Theory Links
Neil V. Murray
Erik Rosenthal
Session 19
Decision Procedure for Autoepistemic Logic
Ilkka Niemela
Logical Matrix Generation and Testing
Peter K. Malkin
Errol P. Martin
Optimal Time Parallel Algorithms for Term Matching
Rakesh M. Verma
I.V. Ramakrishnan
Session 20
Challenge Equality Problems in Lattice Theory
William McCune
Single Axioms in the Implicational Propositional Calculus
Frank Pfenning
Challenge Problems Focusing on Equality and Combinatory Logic:
Evaluating Automated Theorem-Proving Programs
Larry Wos
William McCune
Challenge Problems from Nonassociative Rings for Theorem Provers
Rick Stevens