inference rule markup in W3C specs?

A few of our specs are starting to have
inference rules in them. I'd like to be
able to use those rules in proof systems...
stuff like HELM

I sent some comments to the XQuery folks

They have inference rule markup, but it seems
to be for layout, not for capturing the logical formula.
I told them I like the way the RELAX-NG spec
is built...

The HTML version has inference rules in
a pretty familiar-looking form
and the XML source looks quite usable
as a logical formula

  <rule name="valid">
    <judgement name="match">
      <function name="emptyEnv"/>
      <function name="emptyNamespaceMap"/>
      <function name="emptyBag"/>
      <var range="element"/>
      <var range="pattern"/>
      <var range="keybag"/>
      <var range="keyrefbag"/>
    <judgement name="keyComplete">
      <var range="keybag"/>
      <var range="keyrefbag"/>
      <judgement name="keyConflict">
        <var range="keybag"/>
    <judgement name="valid">
      <var range="element"/>
      <var range="pattern"/>

It occurs to me that the RDF Model Theory spec
has some inference rules; they're so simple
I almost didn't think of them as inference rules,
but they are...

      If E contains:  then add:
rdf1  xxx aaa yyy     aaa rdf:type rdf:Property

A while ago, I looked for inference rule markup
in MathML, but I didn't find any.

After a quick scan of ,
I don't see any tools for taking RuleML and formatting
it for display.

Do other folks produce documents with machine-checkable
inference rules? using XML? How do you do it?

Dan Connolly, W3C

Received on Thursday, 11 April 2002 16:01:20 UTC