Journal of Automated Reasoning (JAR), Volume 5

Volume 5, Number 1, March 1989

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

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

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

Volume 5, Number 2, June 1989

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

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

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

Volume 5, Number 3, September 1989

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

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

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

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 BibTeX
• Warren A. Hunt Jr.: Microprocessor Design Verification. 429-460 BibTeX
• J. Strother Moore: A Mechanically Verified Language Implementation. 461-492 BibTeX
• William D. Young: A Mechanically Verified Code Generator. 493-518 BibTeX
• William R. Bevier: Kit and the Short Stack. 519-530 BibTeX

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

• 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 BibTeX