Copy Link
Add to Bookmark
Report
AIList Digest Volume 6 Issue 079
AIList Digest Friday, 22 Apr 1988 Volume 6 : Issue 79
Today's Topics:
Conferences - CADE-9 Automated Deduction &
Productivity (Preliminary Program)
----------------------------------------------------------------------
Date: Thu, 14 Apr 88 12:02:01 -0500
From: stevens%antares@anl-mcs.arpa
Subject: Conference - CADE-9 Automated Deduction
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
------------------------------
Date: Mon, 18 Apr 88 15:39:46 EST
From: Charles Youman <m14817@mitre.arpa> (youman@mitre.arpa)
Subject: Conference - Productivity (Preliminary Program)
I think the following conference announcement will be of
interest to this group because there are a number of papers being presented
on expert systems.
Preliminary Program -- PRODUCTIVITY: PROGRESS, PROSPECTS, AND PAYOFF
27th Annual Technical Symposium of the Washington DC Chapter of ACM
Gaithersburg, Maryland June 9, 1988
Sponsors:
Washington DC Chapter, Association for Computing Machinery;
Institute for Computer Sciences & Technology, National Bureau
of Standards
Key Dates:
Register by June 1, 1988 and save over 10% of at door rate
Register by May 1, 1988 and save an additional 15%
Special rate for full time students
Productivity is a key issue in the information industry. Information
technology must provide the means to maintain and enhance productivity.
The symposium "Productivity: Progress, Prospects, and Payoff" will
explore theoretical and practical issues in developing and applying
technology in an information-based society.
Keynote address: "Near Term Improvements in Productivity"
Howard Yudkin, President and CEO, Software Productivity Consortium
Plenary panel: "What Are the Impediments to Improving Productivity?"
Walter Douherty, IBM
Phil Kiviat, SAGE Federal Systems
Marshall Potter, U.S. Navy
Al Scherr, IBM
Parallel sessions:
Processes and Tools for Higher Software Economics and Reuse
Software Productivity Uncertainty in Software Requirements
Software Specification Tools Development
Panel-Data Management Standards Expert Systems and Knowledge
A Key to Enhanced Productivity Engineering in Software Engineering
For more information, REPLY to this message -OR- contact the Symposium
General Chairman: Charles E. Youman
DC Chapter ACM (703) 883-6349
P.O. Box 12953 youman@mitre.arpa
Arlington, VA 22209-8953
27th Annual Technical Symposium
Program Schedule
8:00 -- 9:00: Registration
9:00 -- 9:15: Introduction
Welcoming Remarks
Richard L. Muller, DC ACM Chapter Chairman
James Burrows, Director, Institute for Computer Sciences and
Technology, NBS
Introduction of the Candidates for Chapter Office
Presentation of Awards
9:15 -- 10:00: Keynote Address
How Near-Term Productivity Gains Will Be Achieved
Howard L. Yudkin, President and CEO, Software Productivity
Consortium
Dr. Yudkin received his BSEE from the University of Pennsylvania
and both MSEE and PhD degrees from the Massachusetts Institute of
Technology. He has 30 years of experience in management,
engineering, research, and teaching.
Dr. Yudkin is President and Chief Executive Officer of the
Software Productivity Consortium, an organization established by
14 leading aerospace firms to develop tools and methods to
improve the efficiency of software development and the quality of
the product. The Consortium focuses on prototyping and
reusability, exploiting the technologies of systems engineering
and measurement. The organization is developing the components
and configuration techniques by which its sponsor companies can
create advanced development environments for software.
He was formerly with Booz, Allen, and Hamilton, Inc., and the
Computer Sciences Corporation. In government, Dr. Yudkin served
as Deputy Assistant Secretary of Defense with responsibilities
for defense communications systems and many of DoD's command and
control and data processing systems. He also served as an
Assistant Director, Defense Research and Engineering.
10:15 -- 11:00: Plenary Panel
What Are the Impediments to Improving Productivity?
Moderator: Wilma Osborne, Institute for Computer Sciences and
Technology, NBS
Philip J. Kiviat, Vice President, Business Operations, SAGE
Federal Systems, Inc.
Walter Doherty, Technical Consultant for Computing Systems, IBM
T. J. Watson Research Center
Al Scherr, Director of Integrated Applications, IBM Information
Systems Software Development
Marshall R. Potter, Technology Assessment Division, Office of the
Assistant Secretary of the Navy for Financial Management
Mr. Kiviat is Vice President, Business Operations of SAGE Federal
Systems, Inc. He is responsible for the acquisition and
management of application system development projects and the
marketing and sale of SAGE's product line for computer-aided
software engineering. Mr. Kiviat was the first Technical
Director of the Federal Computer Performance Evaluation and
Simulation Center (FEDSIM). He has held previous management
positions with Simulation Associates, Inc., CTEC, Inc., and SEI
Information Technology, and technical positions with United
States Steel Corporation and the RAND Corporation.
Mr. Doherty is currently Technical Consultant for Computing
Systems at IBM's Research Division, T. J. Watson Research Center
in Computing Systems. He also manages the Scientific Systems
Support Laboratory there. He has been Manager of Productivity
and Technology Transfer at IBM Research, an adjunct faculty
member at IBM's SRI, a Distinguished Visitor for the IEEE
Computer Society, and a National Lecturer for ACM. He developed
instrumentation and performance measurement technology and used
those tools to study the human-machine interface and productivity
resulting from the use of computers for the past 20 years.
Dr. Scherr is Director if Integraated Applications, IBM
Information Systems Software Development. He manages the
architecture for application programs to achieve consistency,
portability, and extendability. He is the focal point for
creating and supporting SolutionPac offerings. Earlier in his
career with IBM, Dr. Scherr managed the overall system design,
project office, and system test organizations that coordinated
the efforts of 18 development groups in producing 1.8 million
lines of code for the first release of MVS. Dr. Scherr is an IBM
Fellow.
Mr. Potter directs the Technology Assessment Division within the
Office of the Assistant Secretary of the Navy for Financial
Management. He provides the Department of Navy direction for
joint programs and Navy research and development initiatives
covering the entire information resources area. Prior to this
position, Mr. Potter worked for the Naval Electronic Systems
Command, the Defense Communicatons Engineering Center, the David
Taylor Naval R&D Center, and the National Institutes of Health.
11:10 -- 1:00: Parallel Technical Sessions
Session IA: Processes and Tools for Higher Software Productivity
Session Chairman: Ronald Giusti, The MITRE Corporation
How to Lose Productivity with Productivity Tools
Elliot J. Chikofsky, Index Technology Corporation
Integrating Data and Process for Productive Systems Analysis
Robert Lambert, American Management Systems
What Productivity Increases to Expect from a CASE Environment --
Results of a User Survey
Peter Lempp, SPS Software Products and Services, Inc.
A Program a Day: Software Productivity's Four-Minute Mile
Bruce I. Blum, Johns Hopkins University/Applied Physics Laborato-
ry
Session IB: Software Economics and Reuse
Session Chairman: William Wong, National Bureau of Standards
Software Production Economics: Theoretical Models and Practical
Tools
Chris F. Kemerer, MIT Sloan School of Management
Measureing the Software Development Process
Glen Winemiller, Booz, Allen, and Hamilton, Inc.
Software Reuse -- Key to Enhanced Productivity
John Gaffney, Software Productivity Consortium
Improving Small Systems Software Development Productivity Through
the Management Process
Emily Beaton, The MITRE Corporation
1:00 -- 2:00: Lunch
2:00 -- 3:15: Parallel Technical Sessions
Session IIA: Software Specification Tools
Session Chairman: Walter Ellis, IBM Corporation
Program Visualization as a Technique for Improving Software
Productivity
B. Kjell and P. Wang, George Mason University
Specifying Syntax-Directed Tools and Automating Their
Implementation
Larry Morell and Keith Miller, The College of William and Mary
The Visible Tools Shop: Increasing Programmer Productivity
Through Visual Displays
P. David Stotts, Richard Furuta, and Jefferson Ogata, University
of Maryland
Session IIB: Uncertainty in Software Requirements Development
Session Chairman: James D. Palmer, George Mason University
Impact of Requirements Uncertainty on Software Productivity
James D. Palmer, George Mason University
A Knowledge-Based Requirements System
Dolly Samson, George Mason University
A Knowledge-Based System to Reduce Software Requirements
Volatility
Margaret E. Myers, George Mason University
3:30 -- 4:45: Parallel Technical Sessions
Session IIIA: Panel -- Data Management Standards: A Key to
Enhanced Productivity
Moderator: Elizabeth Fong, National Bureau of Standards
Bruce Bargmeyer, Lawrence Berkeley Laboratory
John Campbell, National Computer Security Center
Joe Leahy, UNISYS
Melody Rood, The MITRE Corporation
Edward Stull, GTE Government Systems
Session IIIB: Expert Systems and Knowledge Engineering in
Software Engineering
Session Chairman: Jon Weyland, Boeing Computer Services
Applying Software Engineering to Knowledge Engineering (and
Vice-Versa)
L. H. Reeker, T. A. Blaxton, and Christopher R. Westphal, The BDM
Corporation
Typed Functional Programming for Rapid Development of Reliable
Software
Val Breazu-Tannen, O. Peter Buneman, and Carl A. Gunter,
University of Pennsylvania
An Experimental Expert System for Improving the Productivity of
Nautical Chart Cartographers
G. F. Swetnam and E. J. Dombroski, The MITRE Corporation
5:00 -- 5:15: Washington DC Chapter ACM Business Meeting
[Contact the message author for registration info. -- KIL]
------------------------------
End of AIList Digest
********************
