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 BibTeX
• Shie-Jue Lee, David A. Plaisted: Eliminating Duplication with the Hyper-Linking Strategy. 25-42 BibTeX
• Dan Benanav: Recognizing Unnecessary Clauses in Resolution Based Systems. 43-76 BibTeX
• Rolf Socher-Ambrosius: How to Avoid the Derivation of Redundant Clauses in Reasoning Systems. 77-97 BibTeX
• Nicola Olivetti: Tableaux and Sequent Calculus for Minimal Entailment. 99-139 BibTeX

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

Volume 9, Number 2, October 1992

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

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

Volume 9, Number 3, 1992

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

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