directives1 http://www.riaca.win.tue.nl/cds/directives/directives1.ocd 2006-06-01 2004-06-01 experimental 1 3 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 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. 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. evaluate_to_type 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. The value of (7*6)/2 is a natural number. The expression below asks for this integer. 76 2 The type of the responded object should be equal to the specification, that is the second argument of the evaluate_to_type. look_up 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. Looking up sin is expressed as follows: response 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. prove 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. disprove 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. 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.***) prove_in_theory 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. find 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. Searching for a real number x such that sin(x) = 0 0 is to be compared to asking for an inverse of x: 0 The body of argument with the binder x replaced by the response should be a true statement. decide This symbol is a function with one argument, which should be a clause. When applied to a clause, it asks whether the clause holds. The question if sin(Pi) is equal to zero can be phrased as follows. 0 The response to the decide query is logically equivalent to the truth of the argument. explore 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. 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. A response R should satisfy the requirement that R implies the assertion.