Journal of Automated Reasoning (JAR), Volume 8

Volume 8, Number 1, February 1992

Studies in Automated Reasoning

David M. Russinoff: A Mechanical Proof of Quadratic Reciprocity. 3-21
Anita Jindal, Ross A. Overbeek, Waldo C. Kabat: Exploitation of Parallel Processing for Implementing High-Performance Deduction Systems. 23-38
Eric Domenjoud: A Technical Note on AC-Unification. The Number of Minimal Unifiers of the Equation alpha x₁ + . . . + alpha x_p =_AC beta y₁ + . . . + beta y_q. 39-44
Larry M. Hines: Completeness of a Prover for Dense Linear Orders. 45-75
Shyi-Ming Chen, Jyh-Sheng Ke, Jin-Fu Chang: An Inexact Reasoning Algorithm Based on Fuzzy Rule Matrix Transformations. 77-90
Art Quaife: Automated Deduction in von Neumann-Bernays-Gödel Set Theory. 91-147

Soumitra Bose, Edmund M. Clarke, David E. Long, Spiro Michaylov: PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses. 153-181
Reinhold Letz, Johann Schumann, Stefan Bayerl, Wolfgang Bibel: SETHEO: A High-Performance Theorem Prover. 183-212
Robert Veroff: The Linked Inference Principle, I: The Formal Treatment. 213-274
James D. Baker, Shariar Zand-Biglari: An Integral Theorem Prover And The Role Of Proof Planning. 275-295
John C. Shepherdson: SLDNF-Resolution with Equality. 297-306

Basic Research Problems

Larry Wos: The Problem of Choosing between Using and Avoiding Eqyality Predicates. 307-309

Dave Barker-Plummer: Gazing: An Approach to the Problem of Definition and Lemma Use. 311-344
Chitta Baral, V. S. Subrahmanian: Stable and Extension Class Theory for Logic Programs and Default Logics. 345-366
Robert J. Hall: Comparing Parameter Schemes for Propositional Reasoning: An Empirical Study. 367-394
Mark F. Russo, Richard L. Peskin: Automatically Identifying the Asymptotic Behavior of Nonlinear Singularly Perturbed Boundary Value Problems. 395-419

Basic Research Problems