- From: Andrea Asperti <asperti@CS.UniBO.IT>
- Date: Fri, 12 Apr 2002 10:32:27 +0200 (CEST)
- To: Dan Connolly <connolly@w3.org>
- cc: www-math@w3.org, www-rdf-logic@w3.org, Harold Boley <boley@informatik.uni-kl.de>, Claudio Sacerdoti_Coen <sacerdot@CS.UniBO.IT>

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