Project No.MERG-CT-2004-012718
supported by the European Commission's Marie Curie Actions Programme : European Reintegration Grants

Project site

The SysteMaThEx project (proposal) aims at providing major case studies of systematic theory exploration using a model for systematic theory exploration recently proposed by Bruno Buchberger [Buchberger 2004b]. Two major case studies were proposed for this project:

• exploration of the theory of tuples and similar theories (strings, sets, bags, trees) to the extent described in literature, for example in [Manna Waldinger 1985], [Gries Schneider 1993],
• exploration of the theory of Groebner Bases to the extent described in literature, for example in [Winkler 1996], [Buchberger 1998].

The case studies will be carried out with the help of the Theorema system, and will have as side effects the refinement of the Theorema system to support the case studies undertaken by the project. The proposal for the project is intended for the Sixth EU Framework Programme for Research and Technologi- cal Development (FP) - Marie Curie Actions, European Reintegration Grants. The participants in this project are:

• a researcher that has spent at least 24 months in a European Project (Adrian Craciun, the author of this report),
• a host institution, in the researchers home country (the Institute e-Austria,Timisoara).

The purpose of this specific programme is to ensure an environment that allows the reintegration of the researcher into his (in this case) home country and which also provides further prospects for the development of a future career in research. The origins of the SysteMaThEx project lay in the work carried out in the Theorema group at the Research Institute for Symbolic Computation under the guidance of Bruno Buchberger. The Theorema system aims to provide computer support to "working mathematicians" (i.e. mathematicians who teach and/or do research in mathematics), in all the phases of the mathematical activities (see [Theorema- Web] for an overall description and documentation, papers - some of which we will refer to throughout this report):

• proving propositions about concepts (introduced by definitions);
• computing using algorithms;
• solving equations, inequations, systems thereof;
• parsing, understanding and further presenting interactive mathematical texts.

Bruno Buchberger has long advocated the "theory exploration paradigm" as opposed to "isolated theorem proving", for example see [Buchberger 2000], [Buchberger 2004b], and the Theorema system is driven proving", for example see [Buchberger 2000], [Buchberger 2004b], and the Theorema system is driven towards supporting the exploration paradigm. In fact Bruno Buchberger had a pivotal role in establishing the new field of Mathematical Knowledge Management (MKM), which tries to address the needs for automated support in the various aspects of doing mathematics - see [MKM 2001], [MKM 2003] (MKM will be introduced in a bit more detail in a following section). One of the most important reasons for setting up the Theorema system, according to Bruno Buchberger, was his (a real working mathematician) need for an automated support tool for the exploration of the theory of Gröbner bases. The SysteMaThEx project is motivated by all of the above, and it aims to make a contribution to the field of MKM by developing knowledge bases through systematic exploration in the two important case studies considered (theory of tuples and theory of Groebner bases).

• [Buchberger 1998] B. Buchberger. Introduction to Gröbner Bases. In: Gröbner Bases and Applications (B. Buchberger, F.Winkler, eds.), London Mathematical Society Lecture Notes Series 251, Cambridge University Press, 1998,pp.331.
• [Buchberger 2000] B. Buchberger. Theory Exploration with Theorema, Analele Universitatii din Timisoara, Seria MatematicaInformatica, Vol. XXXVIII, Fasc. 2, 2000, (Proceedings of SYNASC 2000, 2nd International Workshop on Symbolic and Numeric Algorithms In Scientific Computing, Oct. 46, 2000, Timisoara, Romania T. Jebelean, V. Negru, A. Popovici, eds.), pp.932.
• [Buchberger 2004b] B. Buchberger. Algorithm Supported Mathematical Theory Exploration. In: Proceedings of AISC 2004 (7 th International Conference on Artificial Intelligence and Symbolic Computation), B. Buchberger, John Campbell (ed.), Springer Lecture Notes in Artificial Intelligence Vol. 3249, pp. 236-250. 22-24 September 2004.Copyright: Springer, Berlin-Heidelberg, RISC, Johannes Kepler University, Austria. B. Buchberger and the Theorema group. The Th orem Project @ RISC and RICAM, a presentation brochure for the Theorema Project.
• [Gries Schneider 1993] David Gries, Fred B. Schneider. A Logical Approach to Discrete Math. Springer-Verlag New York 1993.
• [Manna Waldinger 1985] Z. Manna, R. Waldinger, The Logical Basis for Computer Programming - Volume 1 - Deductive Reasoning, Addison-Wesley Publishing Company, ISBN 0201182602 (v. 1), 1985.
• [MKM 2001] B. Buchberger, O. Caprotti (eds.). Mathematical Knowledge Management. Electronic Proceedings of the 1st International Workshop on Mathematical Knowledge Management, RISC, Schloss Hagenberg, Austria, Sep.24-26, 2001, http://www.risc.uni-linz.ac.at/institute/conferences/MKM2001/Proceedings/
• [MKM 2003] A. Asperti, B. Buchberger, J. Davenport. Mathematical Knowledge Management. Proceedings of the Second International Conference on Mathematical Knowledge Management (MKM 2003), Bertinoro, Italy, Feb.16-18, 2003, Lecture Notes in Computer Science,Vol.2594, Springer, Berlin-Heidelberg-New York, 2003, 223 pages.
• [TheoremaWeb] Theorema Web Page: http://www.theorema.org
• [Winkler 1996] F. Winkler, Polynomial algorithms in computer algebra, Springer Verlag Wien 1996.