[Om] Multistep "equation" symbol?

Alberto Gonz ález Palomo Alberto.Gonzalez at matracas.org
Mon May 11 23:01:40 CEST 2009

On Mon, 11 May 2009 14:55:04 +0100 (BST)
"Professor James Davenport" <jhd at cs.bath.ac.uk> wrote:

> On Mon, May 11, 2009 2:37 pm, Lars Hellström wrote:
> > Is there an established OM symbol for "multistep equations" (see
> > example below)? If not, would it make sense as part of some official
> > content dictionary?
> There isn't in OpenMath, but OMDoc may well have thoughts on this - Michael?
> The reason I say that is what you have is really a (part of) a proof here,
> especially when one looks at the annotations.
> As you said, what you have is a proof, which is why I'd rather Michael
> commented.

      I'll comment instead for now, and then he will correct me if
necessary. :-)

      I thought about it some time ago for encoding steps in an
OpenMath-based toy Computer Algebra System I wrote, and my first attempt
was to encode this in OMDoc as a "proof" element, with each step inside
a "derive" element:


      However I'm not satisfied with this: I suspect that the semantically
correct way would be to use an equality (the "claim") in each "derive/FMP",
that is, instead of:

     <derive><FMP>[step 1]</FMP></derive>
     <derive><FMP>[step 2]</FMP></derive>
     <derive><FMP>[step 3]</FMP></derive>

      it would have the following redundant form:

     <derive><FMP>[step 1] = [step 2]</FMP></derive>
     <derive><FMP>[step 2] = [step 3]</FMP></derive>
     <derive><FMP>[step 3] = ...</FMP></derive>

      You could use OMR (references) for either the LHS or the RHS
of the equations to avoid the duplication:

     <derive><FMP>[step 1]        = #2</FMP></derive>
     <derive><FMP>[step 2]{@id=2} = #3</FMP></derive>
     <derive><FMP>[step 3]{@id=3} = ...</FMP></derive>

      This way you (Lars) can have different relations in each step,
as you wanted.

> > Some instances of a relation carry remarks explaining why
> > that step holds.

      This is done with the "method" element inside "derive".

      The relevant section of the OMDoc book is in "Part III: The OMDoc
Document Format" -> "Representing Proofs" -> "Proof Structure", at
page 169 (PDF page 185):


	Alberto González Palomo
	Toledo, España / Saarbrücken, Deutschland

More information about the Om mailing list