Volume 5, Number 1, March 1989

• 
  Vladimir Lifschitz: What Is the Inverse Method? 1-23
• 
  Dallas Lankford: Non-Negative Integer Basis Algorithms for Linear Equations with Integer Coefficients. 25-35
• 
  David A. Wolfram: Intractable Unifiability Problems and Backtracking. 37-47
• 
  Tong Gao Tang: Temporal Logic CTL + PROLOG. 49-65
• 
  S. Purushothaman, P. A. Subrahmanyam: Mechanical Certification of Systolic Algorithms. 67-91

Basic Research Problems

• 
  Larry Wos: The Problem of Finding an Inference Rule for Set Theory. 93-95

Problem Corner

• 
  Art Quaife: Automated Development of Tarski's Geometry. 97-118

Volume 5, Number 2, June 1989

• 
  Avra Cohn: The Notion of Proof in Hardware Verification. 127-139
• 
  Tie-Cheng Wang, Rick Stevens: Solving Open Problems in Right Alternative Rings with Z-Module Reasoning. 141-165
• 
  Teodor C. Przymusinski: On the Declarative and Procedural Semantics of Logic Programs. 167-205
• 
  Kwong-Sak Leung, W. Lam: A Fuzzy Expert System Shell Using Both Exact and Inexact Reasoning. 207-233

Basic Research Problems

• 
  Larry Wos: The Problem of Determining the Size of a Complete Set of Reductions. 235-237

Problem Corner

• 
  Cynthia A. Wick, William McCune: Automated Reasoning about Elementary Point-Set Topology. 239-255

Volume 5, Number 3, September 1989

• 
  Peter B. Andrews: On Connections and Higher-Order Logic. 257-291
• 
  Arcot Rajasekar, Jorge Lobo, Jack Minker: Weak Generalized Closed World Assumption. 293-307
• 
  Ulrich Furbach, Steffen Hölldobler, Joachim F. Schreiber: Horn Equational Theories and Paramodulation. 309-337
• 
  Bruce W. Char, Alan R. Macnaughton, Paul A. Strooper: Discovering Inequality Conditions in the Analytic Solution of Optimization Problems. 339-362
• 
  Lawrence C. Paulson: The Foundation of a Generic Theorem Prover. 363-397

Basic Research Problems

• 
  Larry Wos: The Problem of Guaranteeing the Existence of a Complete Set of Reductions. 399-401

Problem Corner

• 
  Richard Schmid, Hans-Albert Schneider, Thomas Filkorn: Using an Extended PROLOG to Solve the Lion and Unicorn Puzzle. 403-408

Volume 5, Number 4, December 1989

• 
  William R. Bevier, Warren A. Hunt Jr., J. Strother Moore, William D. Young: An Approach to Systems Verification. 411-428
• 
  Warren A. Hunt Jr.: Microprocessor Design Verification. 429-460
• 
  J. Strother Moore: A Mechanically Verified Language Implementation. 461-492
• 
  William D. Young: A Mechanically Verified Code Generator. 493-518
• 
  William R. Bevier: Kit and the Short Stack. 519-530

Basic Research Problems

• 
  Larry Wos: The Problem of Guaranteeing the Absence of a Complete Set of Reductions. 531-532

Problem Corner

• 
  Gregory H. Chisholm, Brian T. Smith, Anthony S. Wojcik: An Automated Reasoning Problem Associated with Proving Claims about Programs Using Floyd-Hoare Inductive Assertin Methods. 533-540