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

inference rule markup?

From: Dan Connolly <connolly@w3.org>
Date: Mon, 12 Feb 2001 12:00:53 -0600
Message-ID: <3A8824D5.2CEE0F09@w3.org>
To: mff@research.att.com, spec-prod@w3.org
CC: "Philip Wadler (Avaya)" <wadler@avaya.com>, "Fuchs, Matthew" <matthew.fuchs@commerceone.com>, asperti@cs.unibo.it, schena@cs.unibo.it

I'm trying to (a) review some of the XML Query stuff,
and (b) research the state-of-the-art in representing
formal knowledge in the web.

e.g. I see you writing these rules ala:

                                             G |- Exp : t 

                                       G |- @Name[Exp]: @Name[t] 



How did you produce that document? I suspect it's converted
from latex; can I look at the source? Is there some
popular latex package used for inference rules?

I'm having trouble parsing it; i.e. figuring out the
implicit operators and precedence in the notation.
(I haven't read the spec very carefully... I wouldn't
be surprised if there's enough information in there,
if I were to read it carfully.)

I was hoping that these rules were really written formally;
i.e. in such a way that I could do certain checks on them
by machine. For example, in translating Wadler's formalization
of XPath to larch a while ago, I found a bug in his paper.

But some of the query rules seem to have "..." and
other informal notation in them; e.g.

We write |- Query1 ... Queryn if the sequence of query items Query1 ...
Queryn is well typed. 
                              G |- environment (Query1),..., environment
                                     G |- Query1      ...      G |-

                                           Query1... Queryn 

Matt Fuchs and I were chatting in the hall at XML 2000, and
the idea of using MathML to produce these specs came up.
I was intrigued by the idea, and I've been noodling on
it ever since.

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.

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

Oops... gotta go to a teleconference... sorry if this doesn't
make any sense...

p.s. spec-prod is a public mailing list; see

Dan Connolly, W3C http://www.w3.org/People/Connolly/
Received on Monday, 12 February 2001 13:01:16 UTC

This archive was generated by hypermail 2.4.0 : Friday, 17 January 2020 19:55:08 UTC