OpenMath Content Dictionary: directives1

Canonical URL:

http://www.riaca.win.tue.nl/cds/directives/directives1.ocd

CD Base:

http://www.openmath.org/cd

CD File:

directives1.ocd

CD as XML Encoded OpenMath:

directives1.omcd

Defines:

decide, disprove, evaluate, evaluate_to_type, explore, find, look_up, prove, prove_in_theory, response

Date:

2004-06-01

Version:

1 (Revision 3)

Review Date:

2006-06-01

Status:

experimental

---

The primal objective of OpenMath objects is to represent mathematical expressions. In this Content Dictionary another objective is addressed, namely to express an action related to a mathematical expression. Such a request for an action is generally referred to as a query. The specific queries are called directives. In this CD we define some. An entity (software) carrying out the query is referred to as a service. The service might return an OpenMath object. To formalize this object, we also introduce the symbol response in this CD.

amc 2004-03-18: added the directive explore. amc 2004-03-24: removed redundancies.

---

evaluate

Description:

This symbol is a function with one argument, which should be a mathematical expression. When applied to a mathematical expression, it asks for an evaluation or simplification of the expression. The evaluation or simplification to be carried out by a service is a simpler mathematical expression (in some definition of complexity of objects) which is equal to the argument.

Example:

The value of sin(Pi) is zero. The expression below asks for sin(Pi) to be evaluated, and so a service receiving the object is supposed to return zero.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
 <OMA><OMS cd="directives1" name="evaluate"/>
      <OMA><OMS cd="transc1" name="sin"/>
           <OMS cd="nums1" name="pi"/>
      </OMA>
 </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="directives1">evaluate</csymbol>
  <apply><csymbol cd="transc1">sin</csymbol><csymbol cd="nums1">pi</csymbol></apply>
 </apply>
</math>

Prefix

evaluate (sin (pi) )

Popcorn

directives1.evaluate(sin(nums1.pi))

Rendered Presentation MathML

$$\mathrm{evaluate}\left(\sin \left(\pi \right)\right)$$

Signatures:

sts

---

[Next: evaluate_to_type] [Last: explore] [Top]

---

evaluate_to_type

Description:

This symbol is a function with two arguments, which should be a mathematical expression and a type. When applied to a mathematical expression E and a type T, it asks for an evaluation or simplification of E to a mathematical expression of type T.

Example:

The value of (7*6)/2 is a natural number. The expression below asks for this integer.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
 <OMA><OMS cd="directives1" name="evaluate"/>
      <OMA><OMS cd="arith1" name="divide"/>
           <OMA><OMS cd="arith1" name="times"/>
                <OMI>7</OMI><OMI>6</OMI>
           </OMA>
           <OMI>2</OMI>
      </OMA>
      <OMS cd="setname1" name="N"/>
 </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="directives1">evaluate</csymbol>
  <apply><csymbol cd="arith1">divide</csymbol>
   <apply><csymbol cd="arith1">times</csymbol>
    <cn type="integer">7</cn>
    <cn type="integer">6</cn>
   </apply>
   <cn type="integer">2</cn>
  </apply>
  <csymbol cd="setname1">N</csymbol>
 </apply>
</math>

Prefix

evaluate (divide (times (7, 6) , 2) , N)

Popcorn

directives1.evaluate((7 * 6) / 2, setname1.N)

Rendered Presentation MathML

$$\mathrm{evaluate}(\frac{7\times 6}{2},\mathbb{N})$$

Commented Mathematical property (CMP):

The type of the responded object should be equal to the specification, that is the second argument of the evaluate_to_type.

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
 <OMATTR>
      <OMATP><OMS cd="ecc" name="type"/>
             <OMV name="T"/>
      </OMATP>
      <OMA><OMS cd="directives1" name="response"/>
           <OMA><OMS cd="directives1" name="evaluate_to_type"/>
                <OMV name="x"/>                     <OMV name="T"/>
           </OMA>
      </OMA>
 </OMATTR>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <semantics>
  <apply><csymbol cd="directives1">response</csymbol>
   <apply><csymbol cd="directives1">evaluate_to_type</csymbol><ci>x</ci><ci>T</ci></apply>
  </apply>
  <annotation-xml cd="ecc" name="type"><ci>T</ci></annotation-xml>
 </semantics>
</math>

Prefix

Attrib([type T ], response (evaluate_to_type ( x, T) ) )

Popcorn

directives1.response(directives1.evaluate_to_type($x, $T)){ecc.type -> $T}

Rendered Presentation MathML

$$\mathrm{response}\left(\mathrm{evaluate\_to\_type}(x,T)\right)$$

Signatures:

sts

---

[Next: look_up] [Previous: evaluate] [Top]

---

look_up

Description:

This symbol is a function with one argument, which should be a mathematical expression. When applied to a mathematical expression, it asks for mathematical expressions related to the argument. If the argument is a single OpenMath symbol, the service might respond by the list of all properties in the CD containing the argument. Alternatively, the service can provide a list of CDs which use the CD in which the argument occurs.

Another service might return all documents in which the symbol occurs.

If the argument is a more complicated object, the same services could be called for, but then with all OpenMath symbols occurring in the argument instead of the single one.

Example:

Looking up sin is expressed as follows:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
 <OMA><OMS cd="directives1" name="look_up"/>
      <OMS cd="transc1" name="sin"/>
 </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML"><apply><csymbol cd="directives1">look_up</csymbol><csymbol cd="transc1">sin</csymbol></apply></math>

Prefix

look_up (sin)

Popcorn

directives1.look_up(sin)

Rendered Presentation MathML

$$\mathrm{look\_up}\left(\sin \right)$$

Signatures:

sts

---

[Next: response] [Previous: evaluate_to_type] [Top]

---

response

Description:

This symbol is a function of one argument, which should be a query. When applied to a query, it refers to the response a service might give. It will mainly be used in this CD to express formal mathematical properties of queries.

Signatures:

sts

---

[Next: prove] [Previous: look_up] [Top]

---

prove

Description:

This symbol is a function with one argument, which should be a clause. When applied to a clause C, it asks for a proof of C.

Signatures:

sts

---

[Next: disprove] [Previous: response] [Top]

---

disprove

Description:

This symbol is a function with one argument, which should be a clause. When applied to a clause C, it asks for a proof of that C does not hold.

Commented Mathematical property (CMP):

Asking to disprove C amounts to asking for a proof that C does not hold. (In other words, this symbol is completely redundant, even in multi-valued logic.***)

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
 <OMA><OMS cd="relation1" name="eq"/>
      <OMA><OMS cd="directives1" name="disprove"/>
           <OMV name="C"/>
      </OMA>
      <OMA><OMS cd="directives1" name="prove"/>
           <OMA><OMS cd="logic1" name="not"/>
                <OMV name="C"/>
           </OMA>
      </OMA>
 </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="directives1">disprove</csymbol><ci>C</ci></apply>
  <apply><csymbol cd="directives1">prove</csymbol>
   <apply><csymbol cd="logic1">not</csymbol><ci>C</ci></apply>
  </apply>
 </apply>
</math>

Prefix

eq (disprove ( C) , prove (not ( C) ) )

Popcorn

directives1.disprove($C) = directives1.prove( not($C))

Rendered Presentation MathML

$$\mathrm{disprove}\left(C\right)=\mathrm{prove}(\neg C)$$

Signatures:

sts

---

[Next: prove_in_theory] [Previous: prove] [Top]

---

prove_in_theory

Description:

This symbol is a function with two arguments, the first of which should be a clause and the second of which should be a symbol indicating a logic theory. When applied to arguments C, T, it asks for a proof of C in theory T.

Signatures:

sts

---

[Next: find] [Previous: disprove] [Top]

---

find

Description:

This symbol is a binder, whose body should be a clause. When bound to a variable (or list of variables) x with body P(x), it asks for a mathematical expression A such that P(A) holds.

Example:

Searching for a real number x such that sin(x) = 0

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
 <OMBIND><OMS cd="directives1" name="find"/>
         <OMBVAR><OMV name="x"/></OMBVAR>
         <OMA><OMS cd="logic1" name="and"/>
              <OMA><OMS cd="set1" name="in"/>
                   <OMV name="x"/><OMS cd="setname1" name="R"/>
              </OMA>
              <OMA><OMS cd="relation1" name="eq"/>
                   <OMA><OMS cd="transc1" name="sin"/><OMV name="x"/></OMA>
                   <OMI>0</OMI>
              </OMA>
         </OMA>
 </OMBIND>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <bind><csymbol cd="directives1">find</csymbol>
  <bvar><ci>x</ci></bvar>
  <apply><csymbol cd="logic1">and</csymbol>
   <apply><csymbol cd="set1">in</csymbol><ci>x</ci><csymbol cd="setname1">R</csymbol></apply>
   <apply><csymbol cd="relation1">eq</csymbol>
    <apply><csymbol cd="transc1">sin</csymbol><ci>x</ci></apply>
    <cn type="integer">0</cn>
   </apply>
  </apply>
 </bind>
</math>

Prefix

find [ x] . (and (in ( x, R) , eq (sin ( x) , 0) ) )

Popcorn

directives1.find[$x -> set1.in($x, setname1.R) and sin($x) = 0]

Rendered Presentation MathML

$$\mathrm{find}\hspace{0.17em}x.x\in \mathbb{R}\wedge \sin \left(x\right)=0$$

is to be compared to asking for an inverse of x:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
 <OMA><OMS cd="directives1" name="evaluate_to_type"/>
      <OMA><OMA><OMS cd="fns1" name="inverse"/>
                <OMS cd="transc1" name="sin"/>
           </OMA>
           <OMI>0</OMI>
      </OMA>
      <OMS cd="setname1" name="R"/>
 </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="directives1">evaluate_to_type</csymbol>
  <apply>
   <apply><csymbol cd="fns1">inverse</csymbol><csymbol cd="transc1">sin</csymbol></apply>
   <cn type="integer">0</cn>
  </apply>
  <csymbol cd="setname1">R</csymbol>
 </apply>
</math>

Prefix

evaluate_to_type (inverse (sin) (0) , R)

Popcorn

directives1.evaluate_to_type(fns1.inverse(sin)(0), setname1.R)

Rendered Presentation MathML

$$\mathrm{evaluate\_to\_type}(\left({\sin }^{-1}\right)\left(0\right),\mathbb{R})$$

Commented Mathematical property (CMP):

The body of argument with the binder x replaced by the response should be a true statement.

Formal Mathematical property (FMP):

OpenMath XML (source)

 <OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMV name="P"/>
       <OMA><OMS cd="directives1" name="response"/>
            <OMBIND><OMS cd="directives1" name="find"/>
                    <OMBVAR><OMV name="x"/></OMBVAR>
                    <OMV name="P"/>
            </OMBIND>
       </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply>
  <ci>P</ci>
  <apply><csymbol cd="directives1">response</csymbol>
   <bind><csymbol cd="directives1">find</csymbol><bvar><ci>x</ci></bvar><ci>P</ci></bind>
  </apply>
 </apply>
</math>

Prefix

P (response (find [ x] . ( P) ) )

Popcorn

$P(directives1.response(directives1.find[$x -> $P]))

Rendered Presentation MathML

$$P\left(\mathrm{response}\left(\mathrm{find}\hspace{0.17em}x.P\right)\right)$$

Signatures:

sts

---

[Next: decide] [Previous: prove_in_theory] [Top]

---

decide

Description:

This symbol is a function with one argument, which should be a clause. When applied to a clause, it asks whether the clause holds.

Example:

The question if sin(Pi) is equal to zero can be phrased as follows.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
 <OMA><OMS cd="directives1" name="decide"/>
      <OMA><OMS cd="relation1" name="eq"/>
           <OMA><OMS cd="transc1" name="sin"/>
                <OMS cd="nums1" name="pi"/>
           </OMA>
           <OMI>0</OMI>
      </OMA>
 </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="directives1">decide</csymbol>
  <apply><csymbol cd="relation1">eq</csymbol>
   <apply><csymbol cd="transc1">sin</csymbol><csymbol cd="nums1">pi</csymbol></apply>
   <cn type="integer">0</cn>
  </apply>
 </apply>
</math>

Prefix

decide (eq (sin (pi) , 0) )

Popcorn

directives1.decide(sin(nums1.pi) = 0)

Rendered Presentation MathML

$$\mathrm{decide}\left(\sin \left(\pi \right)=0\right)$$

Commented Mathematical property (CMP):

The response to the decide query is logically equivalent to the truth of the argument.

Formal Mathematical property (FMP):

OpenMath XML (source)

 <OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
   <OMA><OMS cd="logic1" name="equivalent"/>
        <OMA><OMS cd="directives1" name="response"/>
             <OMA><OMS cd="directives1" name="decide"/>
                  <OMV name="P"/>
             </OMA>
        </OMA>
        <OMV name="P"/>
   </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">equivalent</csymbol>
  <apply><csymbol cd="directives1">response</csymbol>
   <apply><csymbol cd="directives1">decide</csymbol><ci>P</ci></apply>
  </apply>
  <ci>P</ci>
 </apply>
</math>

Prefix

equivalent (response (decide ( P) ) , P)

Popcorn

logic1.equivalent(directives1.response(directives1.decide($P)), $P)

Rendered Presentation MathML

$$\mathrm{response}\left(\mathrm{decide}\left(P\right)\right)\equiv P$$

Signatures:

sts

---

[Next: explore] [Previous: find] [Top]

---

explore

Description:

This symbol is a unary function whose argument should be a mathematical assertion. When applied to an assertion A, it asks for conditions under which the assertion holds.

Example:

Given the Pappos configuration P, the Pappos thesis T asserts that three points of the configuration are collinear. A conceivable answer to the explore directive with the assertion that in configuration P the thesis T holds, is a nondegeneracy condition that makes the assertion valid.

Commented Mathematical property (CMP):

A response R should satisfy the requirement that R implies the assertion.

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
      <OMA><OMS cd="logic1" name="implies"/>
           <OMA><OMS cd="directives1" name="response"/>
                <OMA><OMS cd="directives1" name="explore"/>
                     <OMV name="A"/>                    
                </OMA>
           </OMA>
           <OMV name="A"/>
      </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="directives1">response</csymbol>
   <apply><csymbol cd="directives1">explore</csymbol><ci>A</ci></apply>
  </apply>
  <ci>A</ci>
 </apply>
</math>

Prefix

implies (response (explore ( A) ) , A)

Popcorn

directives1.response(directives1.explore($A)) ==> $A

Rendered Presentation MathML

$$\mathrm{response}\left(\mathrm{explore}\left(A\right)\right)\Rightarrow A$$

Signatures:

sts

---

[First: evaluate] [Previous: decide] [Top]