Hi, I looked at your demo, and I must say it is not clear to me what the demonstration demonstrates. All I learned is that I can click on stuff and get incomprehensible output. What exactly does mbase do? Can it do anything besides retrieving "omdocs" (whatever they are)? Can it prove theorems, for instance? Maybe it would be useful to write a short step-by-step tutorial which contains an example of some useful way of using mbase. A kind of "hello world" example, maybe? -- Peter Michael Kohlhase wrote:

[Apologies for multiple copies]

We are pleased to announce the first official release of

The MBase Mathematical Knowledge Base

MBase 0.8 is available from the MBase web page:

http://www.mathweb.org/mbase/

The MBase system is distributed under the GNU General Public License, binary distributions are provided for Linux and Solaris. An online demo is can be found at

http://mbase.mathweb.org:8080/

Version 0.8 is the first official release of the system. It should be considered as alpha quality code.

ABOUT MBASE

The MBase system is an ongoing development of a web-based knowledge base of formalized mathematics (collections of definitions, theorems, or proofs). The system specializes an SQL-based database system for mathematical structures in the document format OMDoc [1], which is an XML language.

Primary applications of MBase are deduction systems, mathematical assistants, content presentation systems, and learning environments, which can interact with MBase via the MathWeb system, an implementation of a mathematical software bus for distributed theorem proving and symbolic computation [2].

MAJOR FEATURES

-- import & export OMDoc content [1] -- object persistence by standard SQL database system back-end -- pattern-searching (e.g.... search for statements of commutativity) -- web browser interface -- xml-rpc interface for software clients -- multi-platform support (Linux, Solaris, MacOS X)

PLANNED FEATURES (contact us if you want to help)

-- distributed cross-referencing and caching -- content versioning management

Comments, suggestions or bug reports are welcomed and should be directed to the MBase development team <mbase@mathweb.org>.

Have fun, The MBase Team (Andreas Franke, Michael Kohlhase, Markus Moschner)

---

[1] http://www.mathweb.org/omdoc [2] http://www.mathweb.org/mathweb