Journal of Automated Reasoning (JAR), Volume 9

Volume 9, Number 1, August 1992

Studies in Automated Reasoning

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

Basic Research Problems

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

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

Basic Research Problems

Studies in Automated Reasoning

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

Basic Research Problems

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