Journal of Automated Reasoning (JAR), Volume 21

Volume 21, Number 1, August 1998

Hongbo Li, Cheng Minteh: Clifford Algebraic Reduction Method for Automated Theorem Proving in Differential Geometry. 1-21 BibTeX
Hoon Hong, Dalibor Jakus: Testing Positiveness of Polynomials. 23-38 BibTeX
James J. Lu, Neil V. Murray, Erik Rosenthal: A Framework for Automated Reasoning in Multiple-Valued Logics. 39-67 BibTeX
Kenneth Kunen: Nonconstructive Computational Mathematics. 69-97 BibTeX
Christian B. Suttner, Geoff Sutcliffe: The CADE-14 ATP System Competition. 99-134 BibTeX

Larry Wos: Automating the Search for Elegant Proofs. 135-175 BibTeX
Geoff Sutcliffe, Christian B. Suttner: The TPTP Problem Library - CNF Release v1.2.1. 177-203 BibTeX
Andrei Voronkov: Proof Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. 205-231 BibTeX
Jacques Chazarain, Serge Muller: Automated Synthesis of Recursive Programs from a forall-exists Logical Specification. 233-275 BibTeX

John Harrison, Laurent Théry: A Skeptic's Approach to Combining HOL and Maple. 279-294 BibTeX
Andrej Bauer, Edmund M. Clarke, Xudong Zhao: Analytica - An Experiment in Combining Theorem Proving and Symbolic Computation. 295-325 BibTeX
Manfred Kerber, Michael Kohlhase, Volker Sorge: Integrating Computer Algebra into Proof Planning. 327-355 BibTeX
Andreas Dolzmann, Thomas Sturm, Volker Weispfenning: A New Approach for Automatic Theorem Proving in Real Geometry. 357-380 BibTeX
Jinzhao Wu, Zhuojun Liu: Well-Behaved Inference Rules for First-Order Theorem Proving. 381-400 BibTeX