Algorithm-Supported Mathematical Theory Exploration: A Personal View and Strategy - Artificial Intelligence and Symbolic Computation - page 249

4. The Omega System. http://www.ags.uni-sb.de/˜omega/ .
5. A. Asperti, B. Buchberger, and J. H. Davenport, editors. Mathematical Knowl-
edge Management: Second International Conference, MKM 2003 Bertinoro, Italy,
February 16-18, 2003 , volume 2594 of Lecture Notes in Computer Science .
Springer-Verlag, 2003.
6. B. Buchberger. Groebner Rings in Theorema: A Case Study in Functors and Cat-
egories. Technical Report 2003-46, SFB (Special Research Area) Scientific Com-
puting, Johannes Kepler University, Linz, Austria, 2003.
7. B. Buchberger. Towards the automated synthesis of a Grobner bases algorithm.
RACSAM (Review of the Spanish Royal Academy of Sciences) , 2004. To appear.
8. B. Buchberger and A. Craciun. Algorithm synthesis by lazy thinking: Examples
and implementation in Theorema.In Proc. of the Mathematical Knowledge Man-
agement Symposium ,volume93of ENTCS , pages 24-59, Edunburgh, UK, 25-29
November 2003. Elsevier Science.
9. B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, and
W. Windsteiger. The Theorema project: A progress report. In M. Kerber and
M. Kohlhase, editors, Proc. of Calculemus'2000 Conference , pages 98-113, St. An-
drews, UK, 6-7 August 2000.
10. B. Buchberger, G. Gonnet, and M. Hazewinkel, editors. Mathematical Knowledge
Management: Special Issue of Annals of Mathematics and Artificial Intelligence ,
volume 38. Kluwer Academic Publisher, 2003.
11. R. Constable. Implementing Mathematics Using the Nuprl Proof Development
System . Prentice-Hall, 1986.
12. N. G. de Bruijn. The mathematical language automath, its usage, and some of its
extensions. In M. Laudet, D. Lacombe, L. Nolin, and M. Schutzenberger, editors,
Proc. of Symposium on Automatic Demonstration, Versailles, France , volume 125
of LN in Mathematics , pages 29-61. Springer Verlag, Berlin, 1970.
13. M. Gordon and T. Melham. Introduction to HOL : A Theorem Proving Environ-
ment for Higher-Order Logic . Cambridge University Press, 1993.
14. R. Harper. Programming in Standard ML. Carnegie Mellon University. www-
2.cs.cmu.edu/˜rwh/smlbook/online.pdf , 2001.
15. M. Kohlhase. OMDoc: Towards an internet standard for the administration, distri-
bution and teaching of mathematical knowledge. In J.A. Campbell and E. Roanes-
Lozano, editors, Artificial Intelligence and Symbolic Computation: Proc. of the
International Conference AISC'2000 , volume 1930 of Lecture Notes in Computer
Science , pages 32-52, Madrid, Spain, 2001. Springer Verlag.
16. T. Kutsia and B. Buchberger. Predicate logic with sequence variables and sequence
function symbols. In A. Asperti, G. Bancerek, and A. Trybulec, editors, Proc.ofthe
3rd Int. Conference on Mathematical Knowledge Management, MKM'04 ,volume
3119 of Lecture Notes in Computer Science , Bialowieza, Poland, 19-21 September
2004. Springer Verlag. To appear.
17. Zh. Luo and R. Pollack. Lego proof development system: User's manual. Technical
Report ECS-LFCS-92-211, University of Edinburgh, 1992.
18. L. Magnusson and B. Nordstrom. The ALF proof editor and its proof engine. In
H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs , volume 806
of LNCS , pages 213-237. Springer Verlag, 1994.
19. K. Nakagawa. Supporting user-friendliness in the mathematical software system
Theorema. Technical Report 02-01, PhD Thesis. RISC, Johannes Kepler Univer-
sity, Linz, Austria, 2002.
20. L. Paulson. Isabelle: the next 700 theorem provers. In P. Odifreddi, editor, Logic
and Computer Science , pages 361-386. Academic Press, 1990.