Volume 16, Numbers 1-2, March 1996

Automated Mathematical Induction

• 
  François Bronsard, Uday S. Reddy, Robert W. Hasker: Induction Using Term Orders. 3-37
• 
  Deepak Kapur, Mahadevan Subramaniam: New Uses of Linear Arithmetic in Automated Theorem Proving by Induction. 39-78
• 
  Andrew Ireland: Productive Use of Failure in Inductive Proof. 79-111
• 
  Ina Kraan, David A. Basin, Alan Bundy: Middle-Out Reasoning for Synthesis and Induction. 113-145
• 
  David A. Basin, Toby Walsh: A Calculus for and Termination of Rippling. 147-180
• 
  Matt Kaufmann, Paolo Pecchiari: Interaction with the Boyer-Moore Theorem Prover: A Tutorial Study Using the Arithmetic-Geometric Mean Theorem. 181-222

Volume 16, Number 3, June 1996

Studies in Automated Reasoning

• 
  Robert Veroff: Using Hints to Increase the Effectiveness of an Automated Reasoning Program: Case Studies. 223-239

Research Articles

• 
  Peter Baumgartner: Linear and Unit-Resulting Refutations for Horn Theories. 241-319
• 
  Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi: TPS: A Theorem-Proving System for Classical Type Theory. 321-353
• 
  Lusheng Wang, S. K. Michael Wong, Yiyu Yao: On the Completeness of Incidence Calculus. 355-368
• 
  Michael Hedberg: A Type-Theoretic Interpretation of Constructive Domain Theory. 369-425