Journal of Automated Reasoning (JAR), Volume 16

Volume 16, Numbers 1-2, March 1996

• 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

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

• 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