Volume 7, Number 1, March 1991

• 
  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

Basic Research Problems

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

Problem Corner

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

Volume 7, Number 2, June 1991

• 
  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

Basic Research Problems

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

Problem Corner

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

Volume 7, Number 3, September 1991

• 
  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

Basic Research Problems

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

Problem Corner

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

Volume 7, Number 4 December 1991

• 
  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

Basic Research Problems

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

Problem Corner

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