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 http://www.cs.unibo.it/helm/

I sent some comments to the XQuery folks
http://lists.w3.org/Archives/Public/www-xml-query-comments/2002Apr/0016.html

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
http://www.oasis-open.org/committees/relax-ng/proofsystem.html
and the XML source looks quite usable
as a logical formula

--8<--
  <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>
    <judgement name="keyComplete">
      <var range="keybag"/>
      <var range="keyrefbag"/>
    </judgement>
    <not>
      <judgement name="keyConflict">
        <var range="keybag"/>
      </judgement>
    </not>
    <judgement name="valid">
      <var range="element"/>
      <var range="pattern"/>
    </judgement>
  </rule>
--8<--

It occurs to me that the RDF Model Theory spec
  http://www.w3.org/TR/rdf-mt/
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 http://www.dfki.uni-kl.de/ruleml/ ,
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 http://www.w3.org/People/Connolly/

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