suggestions for inference rule markup

Back in Feb 2001, I noticed the inference rules in some XQuery
specs, and asked how they were produced; I'm hoping
to use the inference rules in proof systems like larch/coq
and so on...
  http://lists.w3.org/Archives/Public/spec-prod/2001JanMar/0024.html

I was looking at the specs again today...
  http://www.w3.org/TR/2002/WD-query-semantics-20020326/
and Max showed me how they're produced. The source
looks like, for example:

--8<--
 <infergr>
   <infer>
    <prejudge>
       <clause>
         <expression>(&xq_envv; of &xq_envdyn;)(&gr_Variable;) =
&xd_val; </expression>
       </clause>
     </prejudge>
     <postjudge>
       <clause>
         <environment>&xq_envdyn;</environment>
         <expression>&gr_Variable; &rArr; &xd_val; </expression>
       </clause>
     </postjudge>
   </infer>
 </infergr>
--8<--

That's got more structure than the HTML markup, but it's
still not enough to convert to a logical formula without
character-level parsing of the <expression>s.

Contrast with the RELAX-NG formal semantics
http://www.oasis-open.org/committees/relax-ng/proofsystem.html

where the XML source contains stuff usable as logical
formulas pretty much as is:

--8<--
  <rule name="oneOrMore 1">
    <judgement name="match">
      <var range="env"/>
      <var range="namespaceMap"/>
      <var range="att"/>
      <var range="mixed"/>
      <var range="pattern"/>
      <var range="keybag"/>
      <var range="keyrefbag"/>
    </judgement>

    <judgement name="match">
      <var range="env"/>
      <var range="namespaceMap"/>
      <var range="att"/>
      <var range="mixed"/>
      <element name="oneOrMore">
        <var range="pattern"/>
      </element>
      <var range="keybag"/>
      <var range="keyrefbag"/>
    </judgement>
  </rule>
--8<--

Please consider something like that for the Query specs.

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/

Received on Thursday, 11 April 2002 15:40:10 UTC