From MathWeb

Integrating F-Logic rules in OMDoc for structuring and documenting purposes.

Contents 1 Is OMDoc's XML schema sufficient? 2 Representation of F-Logic 2.1 OpenMath example 3 Discussion

Is OMDoc's XML schema sufficient?

• If yes, find out how to put rules into OMDoc's available statement elements (see the OMDoc specification, chapter 15): definition, axiom, assertion, example may be appropriate.
  • For a less formal structure, i.e. a mere documentation of rules, the text structuring elements of OMDoc (chapter 4.2 and 14) may suffice.
• If no, extend the XML schema, which is available as Relax NG or DTD and designed in a modular way. E.g. introduce a new statement-level element rule

Representation of F-Logic

• F-Logic can either be embedded directly into FMP elements …
• … or it can be encoded in an OpenMath syntax. Lossless transformation from OpenMath to F-Logic would then be possible using XSLT.

OpenMath example

Assuming that symbols for representing F-Logic in OpenMath have been created (This can be done using OMDoc!) and are stored in a content dictionary named flogic, we could translate the F-Logic rule

FORALL X,Y X[son->>Y] <- Y:man[father->X].

to

<FMP>
  <OMOBJ xmlns="http://www.openmath.org/OpenMath">
    <OMA>
      <OMBIND>
        <OMS cd="flogic" name="forall"/>
        <OMBVAR>
          <OMV name="X"/>
          <OMV name="Y"/>
        </OMBVAR>
        <OMA>
          <OMS cd="flogic" name="implies"/>
          <OMA>
            <!-- translation of Y:man[father->X] -->
          </OMA>
          <OMA>
            <!-- translation of X[son->>Y] -->
          </OMA>
        <OMA>
      </OMBIND>
    </OMA>
  </OMOBJ>
</FMP>

See also chapter 13 of the OMDoc specification.

Discussion