W3C home > Mailing lists > Public > www-math@w3.org > April 2002

inference rule markup in W3C specs?

From: Dan Connolly <connolly@w3.org>
Date: 11 Apr 2002 15:01:44 -0500
To: www-math@w3.org
Cc: asperti@cs.unibo.it, Dan Connolly <connolly@w3.org>, www-rdf-logic@w3.org, Harold Boley <boley@informatik.uni-kl.de>
Message-Id: <1018555307.30145.3753.camel@dirk>
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

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

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:27:32 UTC