- 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>
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:21 UTC