Journal of Automated Reasoning (JAR), Volume 4

Volume 4, Number 1, March 1988

• Jaakko Hintikka: Model Minimization - An Alternative to Circumscription. 1-13 BibTeX
• Alan Bundy, Leon Sterling: Meta-Level Inference: Two Applications. 15-27 BibTeX
• Paul Helman, Robert Veroff: Designing Deductive Databases. 29-68 BibTeX
• Franz Oppacher, E. Suen: HARP: A Tableau-Based Theorem Prover. 69-100 BibTeX

• Larry Wos: The Problem of Finding a Strategy to Control Binary Paramodulation. 101-107 BibTeX

Volume 4, Number 2, June 1988

• Robert S. Boyer, J. Strother Moore: The Addition of Bounded Quantification and Partial Functions to A Computational Logic and Its Theorem Prover. 117-172 BibTeX
• Marek Zaionc: Mechanical Procedure for Proof Construction via Closed Terms in Typed \lambda Calculus. 173-190 BibTeX
• Melvin Fitting: First-Order Modal Tableaux. 191-213 BibTeX

• Larry Wos: The Problem of Explaining the Disparate Performance of Hyperresolution and Paramodulation. 215-217 BibTeX

• Art Quaife: Automated Proofs of Löb's Theorem and Gödel's Two Incompleteness Theorems. 219-231 BibTeX

Volume 4, Number 3, September 1988

• Shang-Ching Chou: An Introduction to Wu's Method for Mechanical Theorem Proving in Geometry. 237-267 BibTeX
• Sidney C. Bailin: A lambda-Unifiability Test for Set Theory. 269-286 BibTeX
• David A. Plaisted: Non-Horn Clause Logic Programming Without Contrapositives. 287-325 BibTeX

• Larry Wos: The Problem of Self-Analytically Choosing the Set of Support. 327-329 BibTeX

• Deepak Kapur, Hantao Zhang: Proving Equivalence of Different Axiomatizations of Free Groups. 331-352 BibTeX

Volume 4, Number 4, December 1988

• Mark E. Stickel: A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. 353-380 BibTeX
• Ursula Martin, Tobias Nipkow: Unification in Boolean Rings. 381-396 BibTeX
• Kenneth A. Ross, Rodney W. Topor: Inferring Negative Information from Disjunctive Databases. 397-424 BibTeX
• Klaus Heje Munch: A New Reduction Rule for the Connection Graph Proof Procedure. 425-444 BibTeX
• Leonard G. Monk: Inference Rules Using Local Contexts. 445-462 BibTeX

• Larry Wos: The Problem of Self-Analytically Choosing the Weights. 463-464 BibTeX

• Hans-Jürgen Bürckert, Alexander Herold, Deepak Kapur, Jörg H. Siekmann, Mark E. Stickel, Michael Tepp, Hantao Zhang: Opening the AC-Unification Race. 465-474 BibTeX