[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Axiom-developer] mizar
From: |
root |
Subject: |
[Axiom-developer] mizar |
Date: |
Sat, 17 Jan 2004 16:16:37 -0500 |
David,
Mizar looks like an interesting idea. Carlo Traverso is working
on a literate programming journal. I'll pass the reference on to
him.
This also fits a second goal, the CATS (Computer Algebra Test Suite).
Good work. Thanks.
Tim
==============================================================
Regarding the Axiom Journal, a friend told me about the Mizar project
(http://mizar.org/):
The Mizar project started about 1973 with an attempt to reconstruct
mathematical vernacular.
Since 1989, the most important activity in the Mizar project, apart
from continual improvement of the Mizar System, is the development of
a data base for mathematics. International cooperation (the main
partners: Shinshu University in Nagano and University of Alberta in
Edmonton) resulted in creating a data base which includes more than 2
thousands of definitions of mathematical concepts and more than 30
thousands of theorems.
One interesting point about the project is that they have a journal
(http://mizar.org/JFM/) which seems similar to what Tim wanted for his
Axiom Journal, i.e. with machine readable description of paper content
(http://mizar.org/language/pages/mizar-article.html).
It might be of some interest to look at it before crafting the specs of
the Axiom Journal.
- [Axiom-developer] mizar,
root <=