todo revision 2d6b942b2d10709143b699783f38957d8856e67f
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
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPlan and priority list for CoFI tool activities
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHaskell parser f�r XHaskell erweitern
bea5761c310012308382aa6df7cd80d1f3acc0bcTill MossakowskiDiplom: Encoding for HasCASL in Isabelle/HOL(CF)
bea5761c310012308382aa6df7cd80d1f3acc0bcTill MossakowskiHaskell modules: hiding, renaming
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskidevelopment graph calculus
f1ba3c4b1394e88800bece2e9067e2866015cfebTill Mossakowski- Stack overflow for "show just subtree"
f1ba3c4b1394e88800bece2e9067e2866015cfebTill Mossakowski- view-test7.casl should be provable with globDecomp + locDecopm
f1ba3c4b1394e88800bece2e9067e2866015cfebTill Mossakowski- fail when doing first globDecomp, then local decomp in RelationsAndOrders
4be2c76af9603b48b147f1f369f713e78544974eTill Mossakowski- correct MAYA: glob decomp: some links are not found (Jorina)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskitype check for CASL
e927ace91d729fa35f6b1d08faf84af28cd139e9Till Mossakowski*** Error encode.casl:8.30, No correct typing for
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowskiport CCC to Haskell
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiFunktionen imageOfMorphism und inhabited
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski mit "cvs add SigFuns.hs" einchecken
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski"free datatypes and recursive equations are consistent"
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskicheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiJust True => Yes, is consistent
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiJust False => No, is inconsistent
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiNothing => don't know
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowskicall the symbols in the image of the signature morphism "new"
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski- each new sort must be a free type,
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski i.e. it must occur in a sort generation constraint that is marked as free
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski (Sort_gen_ax constrs True)
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski if not, output "don't know"
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski and there must be one term of that sort (inhabited)
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski if not, output "no"
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski- group the axioms according to their leading operation/predicate symbol,
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski i.e. the f resp. the p in
2d6b942b2d10709143b699783f38957d8856e67fTill Mossakowski forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till Mossakowski forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till Mossakowski Implication Application Strong_equation
2d6b942b2d10709143b699783f38957d8856e67fTill Mossakowski forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till Mossakowski forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till Mossakowski Implication Predication Equivalence
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski if there are axioms not being of this form, output "don't know"
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiZicheng (Till)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiTranslation from CASL with subsorts to CASL without subsorts
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowskisee CATS/basic_encode.sml, encode SubCFOL into CFOL
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowskiencode subsorting by injection functions
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski1. translation of signatures (see HetCATS/CASL/Sign.hs)
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski2. genertion of axioms (injectivity, overloading ...)
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowskidetails: see paper in Theoretical Computer Science, p. 407
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiDarstellung des Logik-Graphen
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskidazu importieren:
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski-- f�r Graph-Darstellung
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskiimport DaVinciGraph
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskiimport GraphDisp
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskiimport GraphConfigure
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski-- f�r Erzeugen von Fenstern
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskiimport TextDisplay
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskiimport Configuration
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskiimport qualified HTk
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskiplus unten genannte Module
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiAufgabe: den Logik-Graph aus folgendem Modul:
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski logicGraph aus Comorphisms/LogicGraph.hs, Typ in Logic/Grothendieck.hs
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskiaufbereiten f�r Anzeige, Vorbild ist in uni/graphs/test/GraphDispTest.hs
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiAufbau von nodeTypeParams
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski-------------------------
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiKnoten (bzw. Kanten) habe Werte, in diesem Fall: AnyLogic (bzw. AnyComorphism)
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskinur 1 Knotentyp, rund, gr�n
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiMen�funktionen AnyLogic -> IO ()
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiValueTitle AnyLogic -> String (= language_name aus Logic/Logic.hs)
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski$$$ ist Funktion zum Zusammenf�gen von Knotentyp-Parametern
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskiunter Men�eintrag "Info" anzeigen: Werte aus Logic/Logic.hs
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskierstmal AnyLogic-Wert auspacken, z.B. mit
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiLogik-Namen ausgbene (mit language_name lid)
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiTest auf Just _, dann String ausgeben
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskiparse_basic_spec lid "Parser for basic specifications"
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskiparse_symb_items lid "Parser for symbol lists"
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskiparse_symb_map_items lid "Parser for symbol maps"
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskiparse_sentence lid "Parser for sentences"
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskibasic_analysis lid "Analysis of basic specifications"
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskidata_logic lid "is a process logic"
f8f7aae3b628450c0d53bd620456da706d4266d3Till Mossakowskimap (sublogic_names lid) (all_sublogics lid)
f8f7aae3b628450c0d53bd620456da706d4266d3Till Mossakowski -- sp�ter besser als eigener Men�punkt ==> eigener Graph
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskimap prover_name (provers lid) -- aus Logic/Provers.hs
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskimap cons_checker_name (cons_checkers lid)
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiAnzeigen dieser Ausgabe mit:
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski createTextDisplay title str [size(100,50)]
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskistr ist der anzuzeigende Inhalt
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiAufbau von arcTypeParams
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski-------------------------
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski- einen "normal" f�r "normale" Comorphismen, schwarz
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski- einen "inclusion" f�r Inclusions, blau
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiKantenmen�: Anzeige von sourceSublogic und targetSublogic (siehe Logic/Comorphisms.hs)
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskimittels language_name
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiAufbau des Graphen selbst
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski------------------------
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiGraphDisp.newGraph daVinciSort -- aus uni/graphs/GraphDisp.hs
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski -- mit leerem globalen Men�
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiAnzeige des Graphen
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski-------------------
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski-------------------------------------------------------------------
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiLaTeX pretty printer
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowskivon Christian:
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowskia) analysierte Formeln und Terme optimal/k�rzer ausgeben:
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowskishorten :: Sign -> {TERM, FORMULA} -> {TERM, FORMULA}
f3a84cc409ed345569be6673d05072dcb4291ebeTill MossakowskiIn Abh�ngigkeit von Sign werden z.B. nicht-�berladene Funktionen
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowskiunqualifiziert ausgeben bzw. zwecks Eindeutigkeit wird (minimal) nur
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowskimit dem Ergebnistyp qualifiziert.
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski((a: Nat) + (b: Nat)): Nat
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowskib) eine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowskiund andere Formate besser zu unterst�tzen und einheitlichen PP code
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowskif�r die CASL Datentypen zu bekommen.
f3a84cc409ed345569be6673d05072dcb4291ebeTill MossakowskiHasCASL hat auch noch keine Mixfix- und Latex Ausgabe.
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski- group the axioms according to their leading operation/predicate symbol,
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski i.e. the f resp. the p in
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski if there are axioms not being of this form, output error
dedca4980b2d43bc343ffcaf73e0617524f9720cTill MossakowskiMissing points for heterogeneous WADT 04 example:
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski- improve display of HasCASL sigs + mors
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiStatic analysis for HasCASL
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder checking class constraints of terms
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder pattern analysis for program equations
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder - for simple types (currently type synonyms)
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder symbol representation
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder symbol map analysis (hiding sub/supertypes)
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian MaederWeak amalgamation analysis?
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian MaederInstantiate Transformation Application system for HasCASL?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAutomatic generation of Haskell (for a HasCASL subset)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiProofs in HasCASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskivisualization of "taxonomy" of CASL signatures
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (subsorts = inheritance, unary preds = concepts, binary preds = relations)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRecognize guarded fragment of CASL:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski G ::= forall x . At(x) => G where At is a conjunction of atoms
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski | exists x . At(x) /\ G
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiJoost Visser wg. ATerms in Haskell => neues Repository
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiBeweise in Isabelle
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCASL consistency checker
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (Vorbild: Larch-Handbuch)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiParser and static analysis for CSP-CASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCASL consistency checker
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIsaWin: support CASL-libraries
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiStatic analysis of architectural specs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
dedca4980b2d43bc343ffcaf73e0617524f9720cTill MossakowskiMissing points for heterogeneous WADT 04 example:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- coding to Isabelle: translate sort gen constraints
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski- correct display of CASL sublogis
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski- extended globDecomp rule: existing local Thm links
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski (e.g. generated by %implied) should lead to fewer new local
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski links ("local composition" rule)
4be2c76af9603b48b147f1f369f713e78544974eTill Mossakowski- Improve adapation to Isabelle's lexis
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIsabelle: (ask Christoph)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski free datatypes
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski prove local thm link (=> green)
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski better interaction between Isabelle instance (for one node)
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski + selection of single goals that are proved
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski => use PGIP interface (Christoph, David)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski correct show theory
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski Keep proofs and lemmas in .thy files (kind of merge)
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski CASL-like syntax
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski CASL annotation for lemmas that should be used in proof
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski inherit CASL's mixfix syntax
04d17d4f8862860f968f6b72b902163aacda6343Till MossakowskiSignatures versus theories: where to store additional infos?
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskicomp(id,x)=x for comorphism names
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiGeneralie CASL2Modal
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiMixfix analysis + typecheck for modality axiomatizations
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiModal logics: modal logic, temporal logic, mu calculus
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski+ translations (e.g. modal to FOL)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiComorphisms: also map of theories; with default definition
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiCASL->Haskell with free DTs (mark sortgens) + recursion
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiCoding of subsorts as unary predicates (for ontologies)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiTranslation between Achim's ontology data structure and CASL (in Hets)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski- List[Dec] wird List[Pos]
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski- George wg. Schlie�en von Fenstern
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski- node numbers do not match
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski- thm links with external target should be provable as well
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRemove warnings
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDifferent types of logic translations
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiImprove Static analysis of structured specs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDevelopment graph calculus, Strategies for DG rules
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiManagement of change
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIntegrate provers
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Otter model checker
2ee1615e999c5e0c49508ed4fcced7344b050042Till Mossakowski FOL-prover by Uli Furhbach
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
f69658e57cba7ecb37c0d84181f4c563215c2534Till Mossakowski Isabelle codings: www.inf.ethz.ch/~vigano
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Renate Schmidt, Manchester: uses FOL prover for description logic
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (as efficient as DL-specific tools!)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Look at PROSPER toolkit
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski consistency: see IJCAR-workshop on non-provability in Cork
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski IJCAR workshop about logical frameworks and meta-languages
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiKlaus' wayfinding example
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUniForM workbench:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskifirst steps towards CASL instance, using ATerms and re-using MMISS instance
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskivariants for specs (needed for DOLCE: CASL variant, DL variant, ...)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIntegration of MAYA and Isabelle/HOL (global HOL-Coding of
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Grothendieck logic)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski + for TAS: reflection of HOL in HOL, to be composed with encodings
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (i.e. signatures, axioms, signature morphisms in HOL,
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski re-use ML signatures) (Einar)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDisplay Specs as daVinci subgraphs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUser interface
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski--------------
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiLogic graph window
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiInput text window
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDevelopment graph window
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiProver windows
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
38f30f746aa42d4fc659a15e183801f2f74596d0Till MossakowskiHets Web interface (cf. CATS/web_interface2.sml)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPackaging of installation
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiintegrate QuickCheck
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiGUI (vgl. VSE)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiincrease performance
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski++++++++++++++++++++++++++++++++++++++++++++++++
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRemaining things
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski++++++++++++++++++++++++++++++++++++++++++++++++
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Coq, PTT in Maude
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiProof general interface (1 day)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiTest Maya with basic datatypes
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiVerbesserung der Fehlermeldungen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiImprove encoding: CATS/basic_encode.sml (3 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMore HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRenamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiExample of Agnes und Frank: proofs in HOL-CASL (2 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiTerm input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiExamples for cond rewriting -> Christophe
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDoku: VSE-Prover, VSE-Method VSE-demo in Bremen?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAdapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiEigene IsaWin-Instanz mit CASL-RS statt HOL-RS
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiEncoding of structured free (3 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiEncoding of structured cofree (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiEingabesyntax als Mix zwischen CASL und HOL (3 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAdapt Isabelle unions to CASL unions (1 week)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIsaWin git/src/isa_ext/casl_thy.sml (1 week)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiGenerate Proof obligations (1 week)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAdd renaming to Isabelle kernel (2 months)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRepository mit korrekten und fehlerhaften Specs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHetCATS User manual, Doku fuer Environments (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiConversion ASF/SDF-Parser -> abstract syntax (in Haskell)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiComparsion of parsers (ML-yacc parser, SDF-Parser)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiConversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPVS anbinden (Kooperation mit Cachan?)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPortations: Intel-Solaris, Mac OS-10 (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiViews on CASL specs: CATS/viewer.sml (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiModule graph CATS/module_graph.sml (1 week) -> Maya?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiATerms via XML: CATS/aterms.sml (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiNeues Tool-Schaubild auf Web-Seiten ver�ffentlichen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiLibrary management: CATS/lib_ana.sml (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiVersion management/Uniform Workbench: CATS/lib_ana.sml (2 months)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski{- This does not work due to needed ordering:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiinstance Functor Set where
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski fmap = mapSet
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiinstance Monad Set where
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski return = unitSet
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski m >>= k = unionManySets (setToList (fmap k m))
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiAufbau von comptable
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski--------------------
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski[("normal","normal","normal"),
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski ("normal","inclusion","normal"),
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski ("inclusion","normal","normal"),
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski ("inclusion","inclusion","inclusion")]
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiAufbau von ginfo
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski--------------------
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiMit initgraphs erzeugen
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiAufbau des Graphen selbst
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski------------------------