Journal of Automated Reasoning (JAR), Volume 26

Volume 26, Number 1, January 2001

Jürgen Giesl: Induction Proofs with Partial Functions. 1-49 BibTeX
Tobias Nipkow: More Church-Rosser Proofs. 51-66 BibTeX
Chih-Hung Wu, Shie-Jue Lee: Parallelization of a Hyper-Linking-Based Theorem Prover. 67-106 BibTeX

Laurent Théry: A Machine-Checked Implementation of Buchberger's Algorithm. 107-137 BibTeX
Wolfgang Gehrke, Jochen Pfalzgraf: Computer-Aided Construction of Finite Geometric Spaces: Automated Verification of Geometric Constraints. 139-160 BibTeX
Matt Kaufmann, J. Strother Moore: Structured Theory Development for a Mechanized Logic. 161-203 BibTeX
Ulrich Berger, Helmut Schwichtenberg, Monika Seisenberger: The Warshall Algorithm and Dickson?s Lemma: Two Examples of Realistic Program Extraction. 205-221 BibTeX

Jürgen Avenhaus, David A. Plaisted: General Algorithms for Permutations in Equational Inference. 223-268 BibTeX
William M. Farmer: STMM: A Set Theory for Mechanized Mathematics. 269-289 BibTeX
Fausto Giunchiglia, Paolo Pecchiari, Carolyn L. Talcott: Reasoning Theories. 291-331 BibTeX

C. A. Johnson: On the Computation of the Disjunctive Well-Founded Semantics. 333-356 BibTeX
M. Randall Holmes, Jim Alves-Foss: The Watson Theorem Prover. 357-408 BibTeX
Robert McNaughton: Semi-Thue Systems with an Inhibitor. 409-431 BibTeX