1<grammar xmlns="http://relaxng.org/ns/structure/1.0" 2 ns="http://relaxng.org/ns/proofsystem"> 3 4<start> 5 <element name="proofSystem"> 6 <oneOrMore> 7 <element name="rule"> 8 <attribute name="name"/> 9 <zeroOrMore> 10 <ref name="antecedent"/> 11 </zeroOrMore> 12 <ref name="consequent"/> 13 </element> 14 </oneOrMore> 15 </element> 16</start> 17 18<define name="formula"> 19 <element name="formula"> 20 <choice> 21 <ref name="judgement"/> 22 <ref name="expr"/> 23 </choice> 24 </element> 25</define> 26 27<define name="consequent"> 28 <ref name="judgement"/> 29</define> 30 31<define name="antecedent"> 32 <ref name="judgement"/> 33</define> 34 35<define name="judgement"> 36 <choice> 37 <element name="judgement"> 38 <attribute name="name"/> 39 <zeroOrMore> 40 <ref name="expr"/> 41 </zeroOrMore> 42 </element> 43 <element name="not"> 44 <ref name="judgement"/> 45 </element> 46 </choice> 47</define> 48 49<define name="expr"> 50 <choice> 51 <element name="var"> 52 <attribute name="range"/> 53 <optional> 54 <attribute name="index"/> 55 </optional> 56 <optional> 57 <attribute name="sub"/> 58 </optional> 59 </element> 60 <element name="function"> 61 <attribute name="name"/> 62 <zeroOrMore> 63 <ref name="expr"/> 64 </zeroOrMore> 65 </element> 66 <element name="element"> 67 <attribute name="name"/> 68 <zeroOrMore> 69 <element name="attribute"> 70 <attribute name="name"/> 71 <ref name="expr"/> 72 </element> 73 </zeroOrMore> 74 <optional> 75 <ref name="context"/> 76 </optional> 77 <zeroOrMore> 78 <ref name="expr"/> 79 </zeroOrMore> 80 </element> 81 <element name="group"> 82 <zeroOrMore> 83 <ref name="expr"/> 84 </zeroOrMore> 85 </element> 86 <element name="string"><text/></element> 87 </choice> 88</define> 89 90<define name="context"> 91 <element name="context"> 92 <ref name="expr"/> 93 </element> 94</define> 95 96</grammar> 97