6. CADE 1982: New York, USA

Donald W. Loveland (Ed.): 6th Conference on Automated Deduction, New York, USA, June 7-9, 1982, Proceedings. Lecture Notes in Computer Science 138 Springer 1982, ISBN 3-540-11558-7

Monday Morning

Larry Wos:
Solving Open Questions with an Automated Theorem-Proving Program. 1-31
Robert E. Shostak, Richard L. Schwartz, P. M. Melliar-Smith:
STP: A Mechanized Logic for Specification and Verification. 32-49
Dale Miller, Eve Longini Cohen, Peter B. Andrews:
A Look at TPS. 50-69

Ewing L. Lusk, William McCune, Ross A. Overbeek:
Logic Machine Architecture: Kernel Funtions. 70-84
Ewing L. Lusk, William McCune, Ross A. Overbeek:
Logic Machine Architecture: Inference Mechanisms. 85-108
S. K. Winker, Larry Wos:
Procedure Implementation Through Demodulation and Related Tricks. 109-131
Bernard Silver:
The Application of Homogenization to Simultaneous Equations. 132-143
Leon Sterling, Alan Bundy:
Meta-Level Inference and Program Verification. 144-150
Richard W. Weyhrauch:
An Example of FOL Using Metatheory. 151-158
Steven Greenbaum, A. Nagasaka, Paul O'Rorke, David A. Plaisted:
Comparison of Natural Deduction and Locking Resolution Implementations. 159-171

Douglas R. Smith:
Derived Preconditions and Their Use in Program Synthesis. 172-193
Chris Goad:
Automatic Construction of Special Purpose Programs. 194-208
Robert E. Shostak:
Deciding Combinations of Theories. 209-222
Tomasz Pietrzykowski, Stan Matwin:
Exponential Improvement of Efficient Backtracking: A Strategy for Plan-Based Deduction. 223-239
Stan Matwin, Tomasz Pietrzykowski:
Exponential Improvement of Efficient Backtracking: data Structure and Implementation. 240-259

Dov M. Gabbay:
Intuitonistic Basis for Non-Monotonic Logic. 260-273
Alan M. Frisch, James F. Allen:
Knowledge Retrieval as Limited Inference. 274-291
Jack Minker:
On Indefinite Databases and the Closed World Assumption. 292-308

Ricardo Caferra:
Proof by Matrix Reduction as Plan + Validation. 309-325
K. M. Hörnig, Wolfgang Bibel:
Improvements of a Tautology-Testing Algorithm. 326-341
Lawrence J. Henschen, Shamim A. Naqvi:
Representing Infinite Sequences of Resolvents in recursive First-Order Horn Databases. 342-359
Ronald V. Book:
The Power of the Church-Rosser Property for String Rewriting Systems. 360-368
Jörg H. Siekmann, Peter Szabó:
Universal Unification and a Classification of Equational Theories. 369-389