External Links

    Journal: Journal of Automated Reasoning

    Volume 4, Issue 4

    353 -- 380Mark E. Stickel. A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler
    381 -- 396Ursula Martin, Tobias Nipkow. Unification in Boolean Rings
    397 -- 424Kenneth A. Ross, Rodney W. Topor. Inferring Negative Information from Disjunctive Databases
    425 -- 444Klaus Heje Munch. A New Reduction Rule for the Connection Graph Proof Procedure
    445 -- 462Leonard G. Monk. Inference Rules Using Local Contexts
    463 -- 464Larry Wos. The Problem of Self-Analytically Choosing the Weights
    465 -- 474Hans-Jürgen Bürckert, Alexander Herold, Deepak Kapur, Jörg H. Siekmann, Mark E. Stickel, Michael Tepp, Hantao Zhang. Opening the AC-Unification Race

    Volume 4, Issue 3

    237 -- 267Shang-Ching Chou. An Introduction to Wu s Method for Mechanical Theorem Proving in Geometry
    269 -- 286Sidney C. Bailin. A lambda-Unifiability Test for Set Theory
    287 -- 325David A. Plaisted. Non-Horn Clause Logic Programming Without Contrapositives
    327 -- 329Larry Wos. The Problem of Self-Analytically Choosing the Set of Support
    331 -- 352Deepak Kapur, Hantao Zhang. Proving Equivalence of Different Axiomatizations of Free Groups

    Volume 4, Issue 2

    117 -- 172Robert S. Boyer, J. Strother Moore. The Addition of Bounded Quantification and Partial Functions to A Computational Logic and Its Theorem Prover
    173 -- 190Marek Zaionc. Mechanical Procedure for Proof Construction via Closed Terms in Typed /lambda Calculus
    191 -- 213Melvin Fitting. First-Order Modal Tableaux
    215 -- 217Larry Wos. The Problem of Explaining the Disparate Performance of Hyperresolution and Paramodulation
    219 -- 231Art Quaife. Automated Proofs of Löb s Theorem and Gödel s Two Incompleteness Theorems

    Volume 4, Issue 1

    1 -- 13Jaakko Hintikka. Model Minimization - An Alternative to Circumscription
    15 -- 27Alan Bundy, Leon Sterling. Meta-Level Inference: Two Applications
    29 -- 68Paul Helman, Robert Veroff. Designing Deductive Databases
    69 -- 100Franz Oppacher, E. Suen. HARP: A Tableau-Based Theorem Prover
    101 -- 107Larry Wos. The Problem of Finding a Strategy to Control Binary Paramodulation
    runs on