Abstract is missing.
- Solving Open Questions with an Automated Theorem-Proving ProgramLarry Wos. 1-31
- STP: A Mechanized Logic for Specification and VerificationRobert E. Shostak, Richard L. Schwartz, P. M. Melliar-Smith. 32-49
- A Look at TPSDale Miller, Eve Longini Cohen, Peter B. Andrews. 50-69
- Logic Machine Architecture: Kernel FuntionsEwing L. Lusk, William McCune, Ross A. Overbeek. 70-84
- Logic Machine Architecture: Inference MechanismsEwing L. Lusk, William McCune, Ross A. Overbeek. 85-108
- Procedure Implementation Through Demodulation and Related TricksS. K. Winker, Larry Wos. 109-131
- The Application of Homogenization to Simultaneous EquationsBernard Silver. 132-143
- Meta-Level Inference and Program VerificationLeon Sterling, Alan Bundy. 144-150
- An Example of FOL Using MetatheoryRichard W. Weyhrauch. 151-158
- Comparison of Natural Deduction and Locking Resolution ImplementationsSteven Greenbaum, A. Nagasaka, Paul O Rorke, David A. Plaisted. 159-171
- Derived Preconditions and Their Use in Program SynthesisDouglas R. Smith. 172-193
- Automatic Construction of Special Purpose ProgramsChris Goad. 194-208
- Deciding Combinations of TheoriesRobert E. Shostak. 209-222
- Exponential Improvement of Efficient Backtracking: A Strategy for Plan-Based DeductionTomasz Pietrzykowski, Stan Matwin. 223-239
- Exponential Improvement of Efficient Backtracking: data Structure and ImplementationStan Matwin, Tomasz Pietrzykowski. 240-259
- Intuitonistic Basis for Non-Monotonic LogicDov M. Gabbay. 260-273
- Knowledge Retrieval as Limited InferenceAlan M. Frisch, James F. Allen. 274-291
- On Indefinite Databases and the Closed World AssumptionJack Minker. 292-308
- Proof by Matrix Reduction as Plan + ValidationRicardo Caferra. 309-325
- Improvements of a Tautology-Testing AlgorithmK. M. Hörnig, Wolfgang Bibel. 326-341
- Representing Infinite Sequences of Resolvents in recursive First-Order Horn DatabasesLawrence J. Henschen, Shamim A. Naqvi. 342-359
- The Power of the Church-Rosser Property for String Rewriting SystemsRonald V. Book. 360-368
- Universal Unification and a Classification of Equational TheoriesJörg H. Siekmann, Peter Szabó. 369-389