OpenMath Content Dictionary: directives1

Canonical URL:

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

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.

xml prefix mathml

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

evaluate (sin (pi) )

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

Signatures:

sts

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.

xml prefix mathml

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

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

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

xml prefix mathml

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

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

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

Signatures:

sts

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:

xml prefix mathml

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

look_up (sin)

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

Signatures:

sts

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

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

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

xml prefix mathml

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

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

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

Signatures:

sts

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

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

xml prefix mathml

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

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

$$\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:

xml prefix mathml

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

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

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

xml prefix mathml

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

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

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

Signatures:

sts

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.

xml prefix mathml

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

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

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

xml prefix mathml

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

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

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

Signatures:

sts

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

xml prefix mathml

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

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

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

Signatures:

sts