References

[Boyer:88] Boyer, R.S., and Moore, J.S.
A Computational Logic Handbook, vol. 23 of Perspectives in computing.
Academic Press Inc., 1988.

[Buchb-Licht:81] Buchberger, B., and Lichtenberger, F.
Mathematics for Computer Science I - The Method of Mathematics (German).
Springer, Berlin, Heidelberg, New York, 1981. Second Edition.

[Buchb-et-al:97]B. Buchberger, T. Jebelean, F. Kriftner, M. Marin, E. Tomuta, D. Vasaru
A Survey of the Theorema Project
Proceedings of ISSAC'97, W. Kuechlin (ed), pp. 384-391, ACM Press, 1997

[Buchb-Vasaru:97] B. Buchberger, D. Vasaru (eds)
Proceedings of the First International Theorema Workshop
RISC Report 97-20, June 1997.

[Clarke-Zhao:93] E. M. Clarke, X. Zhao
Analytica - A theorem prover for Mathematica
The Mathematica Journal 3, 1 (1993), 56-71.

[Constable:86] Constable, R.L., et al.
Implementing Mathematics with the Nuprl Proof Development System.
Prentice-Hall, 1986.

[Dolzmann-Sturm:96] Dolzmann, A., and Sturm, T.
REDLOG User Manual. Edition 1.0 for Version 1.0.
Universitaet Passau, 1996.

[Gordon:93] Gordon, M., and T.F.Melham.
Introduction to HOL: A Theorem Proving Environment for Higher Order Logic.
Cambridge University Press, 1993.

[Homann:96] Homann, K.
Symbolisches Loesen mathematischer Probleme durch Kooperation algorithmischer und deduktiver Systeme (in German).
PhD thesis, Universitaet Karlsruhe, 1996.

[Horn:88] Horn, C.
The Oyster Proof Development System, 1988.

[Huet-et-al:94] Huet, G., Kahn, G., and Paulin-Mohring, C.
The Coq Proof Assistant. A Tutorial. Version 5.10.
INRIA-Rocquencourt, CNRS-ENS Lyon, 1994.

[Paulson:96] L. C. Paulson
Introduction to Isabelle
Computer Laboratory, University of Cambridge.

[vanHermelen:89] van Harmelen, F., Ireland, A., Negrete, S., Smaill, A., and Stevens, A.
The Clam proof planner, 1989.

[Wolfram:96] Wolfram, S.
The Mathematica Book.
Wolfram Media and Cambridge University Press, 1996.