<grammar xmlns="http://relaxng.org/ns/structure/1.0" | |
ns="http://relaxng.org/ns/proofsystem"> | |
<start> | |
<element name="proofSystem"> | |
<oneOrMore> | |
<element name="rule"> | |
<attribute name="name"/> | |
<zeroOrMore> | |
<ref name="antecedent"/> | |
</zeroOrMore> | |
<ref name="consequent"/> | |
</element> | |
</oneOrMore> | |
</element> | |
</start> | |
<define name="formula"> | |
<element name="formula"> | |
<choice> | |
<ref name="judgement"/> | |
<ref name="expr"/> | |
</choice> | |
</element> | |
</define> | |
<define name="consequent"> | |
<ref name="judgement"/> | |
</define> | |
<define name="antecedent"> | |
<ref name="judgement"/> | |
</define> | |
<define name="judgement"> | |
<choice> | |
<element name="judgement"> | |
<attribute name="name"/> | |
<zeroOrMore> | |
<ref name="expr"/> | |
</zeroOrMore> | |
</element> | |
<element name="not"> | |
<ref name="judgement"/> | |
</element> | |
</choice> | |
</define> | |
<define name="expr"> | |
<choice> | |
<element name="var"> | |
<attribute name="range"/> | |
<optional> | |
<attribute name="index"/> | |
</optional> | |
<optional> | |
<attribute name="sub"/> | |
</optional> | |
</element> | |
<element name="function"> | |
<attribute name="name"/> | |
<zeroOrMore> | |
<ref name="expr"/> | |
</zeroOrMore> | |
</element> | |
<element name="element"> | |
<attribute name="name"/> | |
<zeroOrMore> | |
<element name="attribute"> | |
<attribute name="name"/> | |
<ref name="expr"/> | |
</element> | |
</zeroOrMore> | |
<optional> | |
<ref name="context"/> | |
</optional> | |
<zeroOrMore> | |
<ref name="expr"/> | |
</zeroOrMore> | |
</element> | |
<element name="group"> | |
<zeroOrMore> | |
<ref name="expr"/> | |
</zeroOrMore> | |
</element> | |
<element name="string"><text/></element> | |
</choice> | |
</define> | |
<define name="context"> | |
<element name="context"> | |
<ref name="expr"/> | |
</element> | |
</define> | |
</grammar> |