- Donald W. Loveland: Near-Horn Prolog and Beyond. 1-26
- Peter Padawitz: Inductive Expansion: A Calculus for Verifying and Synthesizing Functional and Logic Programs. 27-103

- Larry Wos: The Problem of Finding a Restriction Strategy More Effective Than the Set of Support Strategy. 105-107

- Matt Kaufmann: Generalization in the Presence of Free Variables: A Mechanically-Checked Correctness Proof for one Algorithm. 109-158

- Wu Wen-Tsün: Mechanical Theorem Proving of Differential Geometries and Some of its Applications in Mechanics. 171-191
- Domenico Cantone: Decision Procedures for Elementary Sublanguages of Set Theory: X. Multilevel Syllogistic Extended by the Singleton and Powerset Operators. 193-230
- Domenico Cantone, Jacob T. Schwartz: Decision Procedures for Elementary Sublanguages of Set Theory: XI. Multilevel Syllogistic Extended by Some Elementary Map Constructs. 231-256
- Alfredo Ferro: Decision Procedures for Elementary Sublanguages of Set Theory: XII. Multilevel Syllogistic Extended with Singleton and Choice Operators. 257-270
- Franco Parlamento, Alberto Policriti: Decision Procedures for Elementary Sublanguages of Set Theory: XIII. Model Graphs, Reflection and Decidability. 271-284

- Peter B. Andrews: More on the Problem of Finding a Mapping between Clause Representation and Natural Deduction Representation. 285-286

- Art Quaife: Unsolved Problems in Elementary Number Theory. 287-300

- Alan Bundy, Frank van Harmelen, Jane Hesketh, Alan Smaill: Experiments with Proof Plans for Induction. 303-324
- Rolf Socher: Optimizing the Clausal Normal Form Transformation. 325-336
- Danny De Schreye, Bern Martens, Gunther Sablon, Maurice Bruynooghe: Compiling Bottom-up and Mixed Derivations into Top-down Executable Logic Programs. 337-358
- Allan Ramsay: Generating Relevant Models. 359-368
- Werner Nutt: The Unification Hierarchy is Undecidable. 369-381
- Tong Gao Tang: Programming in Temporal-Nonmonotonic Reasoning. 383-401
- Yishai A. Feldman, Charles Rich: Pattern-Directed Invocation with Changing Equations. 403-433

- Larry Wos: The Problem of Choosing the Type of Subsumption to Use. 435-438

- Matthew Wilding: Proving Matijasevich's Lemma with a Default Arithmetic Strategy. 439-446

- Michael A. McRobbie: Automated Reasoning and Nonclassical Logics: Introduction. 447-451
- John K. Slaney: The Ackermann Constant Theorem: A Computer-Assisted Investigation. 453-474
- Paul Pritchard: Algorithms for Finding Matrix Models of Propositional Calculi. 475-487
- Laurent Catach: TABLEAUX: A General Theorem Prover for Modal Logics. 489-510
- Dov M. Gabbay, Frank Kriwaczek: A Family of Goal Directed Theorem Provers Based on Conjunction and Implication: Part I. 511-536
- Dick De Jongh, Lex Hendriks, Gerard R. Renardel de Lavalette: Computations in Fragments of Intuitionistic Propositional Logic. 537-561
- A. W. Bollen: Relevant Logic Programming. 563-585
- Grigori Mints, Tanel Tammet: Condensed Detachment is Complete for Relevance Logic: A Computer-Aided Proof. 587-596
- Robert K. Meyer, Martin W. Bunder, Lawrence Powers: Implementing the `Fool's Model' of Combinatory Logic. 597-630

- Larry Wos: The Problem of Choosing the Representation, Inference Rule, and Strategy. 631-634

- Paul B. Thistlewaite, Michael A. McRobbie: Approaching Hard Non-Classical Problems. 635-637