inference rule markup?

Mary,

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] 

from

http://lists.w3.org/Archives/Member/w3c-archive/2001Jan/att-0016/01-xmlquery-algebra.html

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.
  http://www.w3.org/XML/9711theory/XPathWadler
  http://www.w3.org/XML/9711theory/XPathWadler.lsl
  http://www.w3.org/XML/9711theory/XPathWadler.html
  http://www.w3.org/XML/9711theory/


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
(Queryn) 
                                     G |- Query1      ...      G |-
Queryn 



                                           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
spec.

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

p.s. spec-prod is a public mailing list; see
http://lists.w3.org/Archives/Public/spec-prod/

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/

Received on Monday, 12 February 2001 13:01:16 UTC