[The articles of this volume will not be reviewed individually.] Contents: {\it Larry Wos}, {\it Ross Overbeek} and {\it Ewing Lusk}, Subsumptions, a sometimes undervalued procedure (pp. 3-40); {\it Hans Jürgen Ohlbach} and {\it Jörg H. Siekmann}, The Markgraf Karl refutation procedure (pp. 41-112); {\it Melvin Fitting}, Modal logic should say more than it does (pp. 113-135); {\it W. W. Bledsoe}, Interactive proof presentation (pp. 136-165); {\it Maurice Bruynooghe}, Intelligent backtracking revisited (pp. 166-177); {\it Alan Bundy}, A science of reasoning (pp. 178-198); {\it Ehud Shapiro}, Inductive inference of theories from facts (pp. 199-254); {\it Jean-Pierre Jouannaud} and {\it Claude Kirchner}, Solving equations in abstract algebras: a rule-based survey of unification (pp. 257-321); {\it Hubert Comon}, Disunification: a survey (pp. 322-359); {\it Deepak Kapur} and {\it Hantao Zhang}, A case study of the completion procedure: proving ring commutativity problems (pp. 360-394); {\it Gérard Huet} and {\it Jean-Jacques Lévy}, Computations in orthogonal rewriting systems. I, II (pp. 395-414, 415-443); {\it Paris C. Kanellakis}, {\it Harry G. Mairson} and {\it John C. Mitchell}, Unification and ML-type reconstruction (pp. 444-478); {\it Mitchell Wand} and {\it Patrick M. O’Keefe}, Automatic dimensional inference (pp. 479-483); {\it Keith L. Clark}, Logic- programming schemes and their implementations (pp. 487-541); {\it Donald W. Loveland} and {\it David W. Reed}, A near-Horn Prolog for compilation (pp. 542-564); {\it P. A. Gardner} and {\it J. C. Shepherdson}, Unfold/fold transformations of logic programs (pp. 565-583); {\it Andrea Corradini} and {\it Ugo Montanari}, An algebraic representation of logic- program computations (pp. 584-612); {\it Jack Minker}, {\it Arcot Rajasekar} and {\it Jorge Lobo}, Theory of disjunctive logic programs (pp. 613-639); {\it Jeffrey F. Naughton} and {\it Raghu Ramakrishnan}, Bottom-up evaluation of logic programs (pp. 640-700); {\it E. W. Elcock}, Asys, the first logic-programming language: a view of the inevitability of logic programming (pp. 701-721).