Journal of Automated Reasoning (JAR), Volume 5

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

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

• 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

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

• 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

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

• 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

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

• 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