[Om] Multistep "equation" symbol?

[Alberto Gonz ález Palomo]

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:

  ...
  <proof>
    <derive><FMP>$sqrt(n^2+1)-1$</FMP></derive>
    <derive>...</derive>
    ...
    <derive><FMP>$1/2n$</FMP></derive>
  </proof>
  ...

      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:

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

      it would have the following redundant form:

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

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

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

      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):

http://www.mathweb.org/omdoc/pubs/omdoc1.2.pdf

      Cheers,
--
	Alberto González Palomo
	Toledo, España / Saarbrücken, Deutschland
	http://www.matracas.org