Journal of Automated Reasoning (JAR), Volume 9

Volume 9, Number 1, August 1992

• William McCune: Automated Discovery of New Axiomatizations of the Left Group and Right Group Calculi. 1-24
• Shie-Jue Lee, David A. Plaisted: Eliminating Duplication with the Hyper-Linking Strategy. 25-42
• Dan Benanav: Recognizing Unnecessary Clauses in Resolution Based Systems. 43-76
• Rolf Socher-Ambrosius: How to Avoid the Derivation of Redundant Clauses in Reasoning Systems. 77-97
• Nicola Olivetti: Tableaux and Sequent Calculus for Minimal Entailment. 99-139

• Larry Wos: The Problem of Demodulation During Inference Rule Application. 141-143

Volume 9, Number 2, October 1992

• Larry Wos: Note on McCune's Article on Discrimination Trees. 145-146
• William McCune: Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval. 147-167
• Mark Franzen: Hilbert's Tenth Problem is of Unification Type Zero. 169-178
• Michael Kifer, Eliezer L. Lozinskii: A Logic for Reasoning with Inconsistency. 179-215
• Donald E. Brown, Wendy J. Markert: Uncertainty Management with Imprecise Knowledge with Application to Design. 217-230
• Nevin Heintze, Spiro Michaylov, Peter J. Stuckey: CLP(R) and Some Electrical Engineering Problems. 231-260
• Deepak Kapur, Paliath Narendran: Complexity of Unification Problems with Associative-Commutative Operators. 261-288

• Larry Wos: The Problem of Demodulator Adjunction. 289-290

Volume 9, Number 3, 1992

• Kenneth Kunen: Single Axioms for Groups. 291-308
• Arnon Avron, Furio Honsell, Ian A. Mason, Robert Pollack: Using Typed Lambda Calculus to Implement Formal Systems on a Machine. 309-354
• Matt Kaufmann: An Extension of the Boyer-Moore Theorem Prover to Support First-Order Quantification. 355-372
• Jean-Louis Lassez, Michael J. Maher: On Fourier's Algorithm for Linear Arithmetic Constraints. 373-379
• Gabriel M. Kuper, Ken McAloon, Krishna V. Palem, Kenneth J. Perry: A Note on the Parallel Complexity of Anti-Unification. 381-389
• Arthur L. Delcher, Simon Kasif: Efficient Parallel Term Matching and Anti-Unification. 391-406

• Larry Wos: The Problem of Demodulating Across Argument and Literal Boundaries. 407-408