- From: Andrea Asperti <asperti@CS.UniBO.IT>
- Date: Tue, 13 Feb 2001 16:31:09 +0100 (CET)
- To: Dan Connolly <connolly@w3.org>
- cc: mff@research.att.com, spec-prod@w3.org, "Philip Wadler (Avaya)" <wadler@avaya.com>, "Fuchs, Matthew" <matthew.fuchs@commerceone.com>, schena@CS.UniBO.IT
Hallo. > > Recently, I found some folks using MathML to work with > proof checking systems; I am digging around their source > code, but I haven't figured out exactly how they represent > inference rules, axioms, theorems and such. The underlying Proof Engine (at present) is the COQ Proof assistant of INRIA-Rocquencourt. But we expect that our methodology should scale to any other Logical Environment or Computer Algebra System, or whatever inference system you have in mind. "COQ on line" is currently broken, but it should be "on" again in a few days. > > HELM http://www.cs.unibo.it/~asperti/HELM/home.html > > Amaya supports presentation MathML... I wonder if it's > got enough stuff to edit specs like the query algebra > spec. If you just need a MathML editor, our widget works much better than Amaya, Mozilla, WebEQ and company. http://www.cs.unibo.it/helm/software/index.html I hope HELM will be mentioned in your report on the state-of-the-art in representing formal knowledge in the web. Please, use the following url: http://www.cs.unibo.it/helm By the way, Dan, we should eventually move MathML inside the Semantic Web area, or at least open a new WG in that direction. MathML has been the first WWW project putting emphasis on "semantics." -- andrea
Received on Tuesday, 13 February 2001 10:31:27 UTC