-
Notifications
You must be signed in to change notification settings - Fork 10
/
Copy pathdirectives1.omcd
343 lines (343 loc) · 13.9 KB
/
directives1.omcd
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
<OMOBJ xmlns:om="http://www.openmath.org/OpenMath"
xmlns="http://www.openmath.org/OpenMath">
<OMA>
<OMS cd="meta" name="CD"/>
<OMA>
<OMS cd="meta" name="CDName"/>
<OMSTR>directives1</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="CDBase"/>
<OMSTR>http://www.openmath.org/cd</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="CDURL"/>
<OMSTR>http://www.riaca.win.tue.nl/cds/directives/directives1.ocd</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="CDReviewDate"/>
<OMSTR>2006-06-01</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="CDDate"/>
<OMSTR>2004-06-01</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="CDStatus"/>
<OMSTR>experimental</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="CDVersion"/>
<OMSTR>1</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="CDRevision"/>
<OMSTR>3</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="Description"/>
<OMSTR>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.</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="CDDefinition"/>
<OMA>
<OMS cd="meta" name="Name"/>
<OMSTR>evaluate</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="Description"/>
<OMSTR>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.</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="Example"/>
<OMSTR>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.</OMSTR>
<OMA>
<OMS cd="directives1" name="evaluate"/>
<OMA>
<OMS cd="transc1" name="sin"/>
<OMS cd="nums1" name="pi"/>
</OMA>
</OMA>
</OMA>
</OMA>
<OMA>
<OMS cd="meta" name="CDDefinition"/>
<OMA>
<OMS cd="meta" name="Name"/>
<OMSTR>evaluate_to_type</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="Description"/>
<OMSTR>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.</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="Example"/>
<OMSTR>The value of (7*6)/2 is a natural number. The expression below asks for this integer.</OMSTR>
<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>
</OMA>
<OMA>
<OMS cd="meta" name="CMP"/>
<OMSTR>The type of the responded object should be equal to the specification, that is the second argument of the evaluate_to_type.</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="FMP"/>
<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>
</OMA>
</OMA>
<OMA>
<OMS cd="meta" name="CDDefinition"/>
<OMA>
<OMS cd="meta" name="Name"/>
<OMSTR>look_up</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="Description"/>
<OMSTR>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.</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="Example"/>
<OMSTR>Looking up sin is expressed as follows:</OMSTR>
<OMA>
<OMS cd="directives1" name="look_up"/>
<OMS cd="transc1" name="sin"/>
</OMA>
</OMA>
</OMA>
<OMA>
<OMS cd="meta" name="CDDefinition"/>
<OMA>
<OMS cd="meta" name="Name"/>
<OMSTR>response</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="Description"/>
<OMSTR>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.</OMSTR>
</OMA>
</OMA>
<OMA>
<OMS cd="meta" name="CDDefinition"/>
<OMA>
<OMS cd="meta" name="Name"/>
<OMSTR>prove</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="Description"/>
<OMSTR>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.</OMSTR>
</OMA>
</OMA>
<OMA>
<OMS cd="meta" name="CDDefinition"/>
<OMA>
<OMS cd="meta" name="Name"/>
<OMSTR>disprove</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="Description"/>
<OMSTR>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.</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="CMP"/>
<OMSTR>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.***)</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="FMP"/>
<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>
</OMA>
</OMA>
<OMA>
<OMS cd="meta" name="CDDefinition"/>
<OMA>
<OMS cd="meta" name="Name"/>
<OMSTR>prove_in_theory</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="Description"/>
<OMSTR>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.</OMSTR>
</OMA>
</OMA>
<OMA>
<OMS cd="meta" name="CDDefinition"/>
<OMA>
<OMS cd="meta" name="Name"/>
<OMSTR>find</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="Description"/>
<OMSTR>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.</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="Example"/>
<OMSTR>Searching for a real number x such that sin(x) = 0</OMSTR>
<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>
<OMSTR>is to be compared to asking for an inverse of x:</OMSTR>
<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>
</OMA>
<OMA>
<OMS cd="meta" name="CMP"/>
<OMSTR>The body of argument with the binder x replaced by the response should be a true statement.</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="FMP"/>
<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>
</OMA>
</OMA>
<OMA>
<OMS cd="meta" name="CDDefinition"/>
<OMA>
<OMS cd="meta" name="Name"/>
<OMSTR>decide</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="Description"/>
<OMSTR>This symbol is a function with one argument, which should be a clause. When applied to a clause, it asks whether the clause holds.</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="Example"/>
<OMSTR>The question if sin(Pi) is equal to zero can be phrased as follows.</OMSTR>
<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>
</OMA>
<OMA>
<OMS cd="meta" name="CMP"/>
<OMSTR>The response to the decide query is logically equivalent to the truth of the argument.</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="FMP"/>
<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>
</OMA>
</OMA>
<OMA>
<OMS cd="meta" name="CDDefinition"/>
<OMA>
<OMS cd="meta" name="Name"/>
<OMSTR>explore</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="Description"/>
<OMSTR>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.</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="Example"/>
<OMSTR>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.</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="CMP"/>
<OMSTR>A response R should satisfy the requirement that R implies the assertion.</OMSTR>
</OMA>
<OMA>
<OMS cd="meta" name="FMP"/>
<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>
</OMA>
</OMA>
</OMA>
</OMOBJ>