Journal of Automated Reasoning (JAR), Volume 16

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 BibTeX
Deepak Kapur, Mahadevan Subramaniam: New Uses of Linear Arithmetic in Automated Theorem Proving by Induction. 39-78 BibTeX
Andrew Ireland: Productive Use of Failure in Inductive Proof. 79-111 BibTeX
Ina Kraan, David A. Basin, Alan Bundy: Middle-Out Reasoning for Synthesis and Induction. 113-145 BibTeX
David A. Basin, Toby Walsh: A Calculus for and Termination of Rippling. 147-180 BibTeX
Matt Kaufmann, Paolo Pecchiari: Interaction with the Boyer-Moore Theorem Prover: A Tutorial Study Using the Arithmetic-Geometric Mean Theorem. 181-222 BibTeX

Studies in Automated Reasoning

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

Research Articles

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