Date: Thu 21 Apr 1988 21:57-PDT From: AIList Moderator Kenneth Laws Reply-To: AIList@KL.SRI.COM Us-Mail: SRI Int., 333 Ravenswood Ave., Menlo Park, CA 94025 Phone: (415) 859-6467 Subject: AIList V6 #79 - Conferences: Automated Deduction, Productivity To: AIList@KL.SRI.COM Status: R 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 (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 ********************