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
  

Last update Mon May 20 01:08:54 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page