Re: inference rule markup in W3C specs?

MathML supports implication, and the difference between an implication
and an inference rule is quite smooth (it is most a matter of notation).
If you strongly plea for having a specific markup for inference rules,
I guess the issue could be considered inside MathML. 
Since we have MathML, it would be nice to be able to use it wherever
it makes sense (i.e. in every context where you need some mathematical
content). 
More generally, the MathML WG is becoming sensible to the problem
of extending the content language beyond the K12 fragment. 
My only fear, in this case, is that the "intended domain" is not
so clear to suggest a sufficiently standard and uniform content markup.
Do you have a clear idea of what you need? For instance, what
kind of datatypes would you like to consider? Would you like
to work in a typed or an untyped formal setting? etc. etc. 

In any case, a strong coordination with the MathML WG is surely 
auspicable. Maybe we can try to create a small task force of people
interested in this issue. But the first problem is surely to
have a beeter understanding of what you (we) are looking for.
	
						-- andrea


On 11 Apr 2002, Dan Connolly wrote:

> 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 Friday, 12 April 2002 04:32:33 UTC