W3C home > Mailing lists > Public > spec-prod@w3.org > January to March 2001

Re: inference rule markup?

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
Message-ID: <Pine.LNX.4.21.0102131617350.13616-100000@marcello.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 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Saturday, 10 March 2012 06:19:11 GMT