todo revision 0ef6fed7a5d52b1f791926bd8a432723ffd28767
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
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPlan and priority list for CoFI tool activities
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski************************************************
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski************************************************
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till MossakowskiSuchfunktion f�r einen Knoten im DG:
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski welche anderen Knoten sind hier mit Theoriemorphismus abbildbar?
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski erstmal auf eine Logik (z.B. CASL) beschr�nken
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski - Funktion f�r Morphismus-Suche zwischen Theorien
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski - evtl. angucken: CASL.SymbolMapAnalysis, inducedFromToMorphism Map.empty
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski RawSymbolMap als "Suche-Guide" wird erestzt durch Axiome/Theoreme
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski - Einbindung ins GUI (GUI.ConvertAbstractToDevGraph)
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till MossakowskiBasicProof in Proofs.Proofs: sind Datenstrukturen f�r informelle Beweise OK?
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till MossakowskiKonfidenzgrade von Beweisen?
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowskivon Till/Jorina (jfgerken@tzi.de) zu erledigen:
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till MossakowskiRepr�sentation �ndern:
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowski Beweisobjekte an DGs, nicht an Regeln
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowski F�r Theoreme in Theorien an Beweisobjekte
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowski BasicProof mit Liste von Beweisobjekten
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowski Isabelles Beweisobjekte einbinden
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowski Definitionen auszeichnen
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill MossakowskiFlorian (Till)
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill MossakowskiHetCATS, uni und CASL-lib auschecken
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowskiabstrakte Syntax f�r ConstraintCASL (s. CASL-lib/ConstraintCASL/)
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski nach HetCATS/ConstraintCASL/AS_ConstraintCASL.der.hs
0e3db835d379ceb594b0daa25a0590abb755a1acTill MossakowskiParser f�r ConstraintCASL
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski nach HetCATS/ConstraintCASL/Parse_AS_Basic.hs
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski hets -o ast.het CASL-lib/ConstraintCASL/RCC8.het
0e3db835d379ceb594b0daa25a0590abb755a1acTill MossakowskiFreiburger Constraint-Solver angucken
0e3db835d379ceb594b0daa25a0590abb755a1acTill MossakowskiBremer Constraint-Solver angucken
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski************************************************
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski************************************************
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowskiport CCC to Haskell
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill MossakowskiFunktionen imageOfMorphism und inhabited
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski mit "cvs add SigFuns.hs" einchecken
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski"free datatypes and recursive equations are consistent"
0e3db835d379ceb594b0daa25a0590abb755a1acTill MossakowskicheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
0e3db835d379ceb594b0daa25a0590abb755a1acTill MossakowskiJust True => Yes, is consistent
e2143dde7e5adcc35f1587e94c9279d8cbe3cbd5Till MossakowskiJust False => No, is inconsistent
e2143dde7e5adcc35f1587e94c9279d8cbe3cbd5Till MossakowskiNothing => don't know
e2143dde7e5adcc35f1587e94c9279d8cbe3cbd5Till Mossakowskicall the symbols in the image of the signature morphism "new"
4a573a1ca4f8556b77e3467e6c2b261ba03e3036Till Mossakowski- each new sort must be a free type,
4a573a1ca4f8556b77e3467e6c2b261ba03e3036Till Mossakowski i.e. it must occur in a sort generation constraint that is marked as free
4a573a1ca4f8556b77e3467e6c2b261ba03e3036Till Mossakowski (Sort_gen_ax constrs True)
e2143dde7e5adcc35f1587e94c9279d8cbe3cbd5Till Mossakowski such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
e2143dde7e5adcc35f1587e94c9279d8cbe3cbd5Till Mossakowski if not, output "don't know"
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski and there must be one term of that sort (inhabited)
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski if not, output "no"
db373255bd95ce4de47dde876c3a3bfc49c22a97Till Mossakowski- group the axioms according to their leading operation/predicate symbol,
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski i.e. the f resp. the p in
db373255bd95ce4de47dde876c3a3bfc49c22a97Till Mossakowski forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
db373255bd95ce4de47dde876c3a3bfc49c22a97Till Mossakowski forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowski Implication Application Strong_equation
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowski forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowski forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowski Implication Predication Equivalence
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowski if there are axioms not being of this form, output "don't know"
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowskicheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowskicheck' [] = ([([],[])],emptyUniqSet)
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowski-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowskicheck' [EqnInfo n ctx ps (MatchResult CanFail _)]
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowskicheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski | all_vars ps = (pats, addOneToUniqSet indexs n)
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski (pats,indexs) = check' rs
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski-- falls ein Konstruktor dabei ist: split_by_constructor
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowskicheck' qs@((EqnInfo n ctx ps result):_)
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski | all_vars ps = ([], unitUniqSet n)
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski | constructors = split_by_constructor qs
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski | only_vars = first_column_only_vars qs
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski | otherwise = panic "Check.check': Not implemented :-("
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski -- Note: RecPats will have been simplified to ConPats
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski -- at this stage.
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski constructors = or (map is_con qs)
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski only_vars = and (map is_var qs)
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowskisubsort definitions: are conservative if formula is satisfiable
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski (generate proof obligation)
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski************************************************
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski************************************************
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill MossakowskiOWL-DL (<)-> CASL-DL
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski highlight does not work properly for HasCASL/Set.het or UserManual/Sbcs.casl
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski some operation symbols
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski show hets output immediately
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski C-c C-g for hets -g
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski when hets terminates abnormally (e.g. with a fail), emacs loops
3c8c05dc3358d217513d8e0e8e32ccd3e4947c05Florian Mossakowski C-n jumps to the next error, but the message windows is not always scrolled
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski in such a way that the error is at the top (for long error lists)
3c8c05dc3358d217513d8e0e8e32ccd3e4947c05Florian Mossakowski Version for XEamcs?
3c8c05dc3358d217513d8e0e8e32ccd3e4947c05Florian Mossakowski should work with parser error messages as well (adapt these?)
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski************************************************
3c8c05dc3358d217513d8e0e8e32ccd3e4947c05Florian Mossakowski************************************************
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill MossakowskiModal-CASL <-> CASL-DL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski see Chapter 4 of "The Description Logic Handbook"
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski and ask Klaus for a print out of it
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski************************************************
198093ec9afd8b459087dc30c94347bb7eeaa282Till Mossakowski************************************************
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till MossakowskiUni-Refactoring,
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till Mossakowskimake modules hierarchical, change scoped type variables for ghc-6.5
198093ec9afd8b459087dc30c94347bb7eeaa282Till Mossakowski(and older ghcs), replace deprecated code (i.e. FiniteMap, hslibs),
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowskiuse HaXml as a cabalized library, provide uni as (one?) cabal
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maederpackage(s), uni used to work under windows as well, watch the
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowskii.e. FilePath, Process discussions (libraries@haskell.org)
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowskipossibly switch to a subversion repository, talk to Achim
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski(amahnke@tzi.de)
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski************************************************
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski************************************************
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowskidevelopment graph calculus
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski(see Sect. IV:4.4 of the CASL Reference Manual)
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowskiimplement simplified rule Theorem-Hide-Shift
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowskitry out examples
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maederconservativity calculus
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowskiweakly amalgamable cocones
38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowskiport hets to windows.
b04658442a4419349d41c931f2a3bda49e8be9e8Till MossakowskiIf hets should become successful then requests for support under
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowskiwindows will surely follow.
b04658442a4419349d41c931f2a3bda49e8be9e8Till MossakowskiGhc, uni and uDrawGraph should work under windows. Only Isabelle does
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowskinot exist for windows, but SPASS does. Probably only a few path
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowskicomputations need to be adapted (made modular) within hets. Also
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowskiposition computations (of Parsec) should be checked under windows.
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski************************************************
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski************************************************
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowskirefactor pretty printing
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowskieine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowskiund andere Formate besser zu unterst�tzen und einheitlichen PP code
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski(independent from GlobalAnnos) f�r die (Het-)CASL (and HasCASL!)
ed892c579cca270fff0aa9cc2a34351c420e3182Till MossakowskiDatentypen (particularly for HasCASL data types) zu bekommen.
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian MaederLaTeX: see listings.sty for LaTeX generation (cf. CoSiT paper)
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski************************************************
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski************************************************
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowskieinfaches Merge von lokalen Beweisen eines abgespeichteren DG
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski in aktuellen DG
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski************************************************
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowskiremaining stuff
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski************************************************
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowskiset up a ticket and tracking systems (for bugs and features) instead
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowskiof this messy todo list
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowskiunify GUI/AbstractGraphView.hs and Taxonomy/AbstractGraphView.hs (make
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowskiit really abstract), possibly contact amahnke@tzi.de regarding
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowskiset up default simplifier
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowskiset up default tactics using axioms
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski (see DOLCE sample files)
2d6b942b2d10709143b699783f38957d8856e67fTill Mossakowskiimprove efficiency (e.g. of UserManual/Sbcs.casl), using profiling
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till Mossakowskidevelopment graph calculus
2d6b942b2d10709143b699783f38957d8856e67fTill Mossakowski- Stack overflow for "show just subtree"
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till Mossakowski- view-test7.casl should be provable with globDecomp + locDecopm
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till Mossakowski- fail when doing first globDecomp, then local decomp in RelationsAndOrders
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski- correct MAYA: glob decomp: some links are not found (Jorina)
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski- Fail: No match in record selector Static.DevGraph.dgn_sign
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski for local subsume in RelationsAndOrders
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski************************************************
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski************************************************
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskigenerate infrastructure for circular coinduction
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian MaederCCS example: commutativity of || by coinduction
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski************************************************
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski************************************************
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskicollect the patches for programatica (or create a package)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski- conv (SN i p) = PN i (S p)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski+ conv (SN i p) = PN i (Sn (show i) p)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskiin programatica/tools/base/parse2/NumberNames.hs
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskifixes translation error of Pair
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskisimplification of HasCASL sentences (omit types)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiLogic COL is a ruin (with wrongly qualified module names)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskilogic coding from the comand line with printing of results
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiHaskell modules: hiding, renaming
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maeder- group the axioms according to their leading operation/predicate symbol,
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski i.e. the f resp. the p in
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
a1bb9f8f9143aa2d84dfab69ed988d94f7e3b196Till Mossakowski forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
a1bb9f8f9143aa2d84dfab69ed988d94f7e3b196Till Mossakowski if there are axioms not being of this form, output error
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMissing points for heterogeneous WADT 04 example:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- improve display of HasCASL sigs + mors
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiStatic analysis for HasCASL
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich pattern analysis for program equations
e1f2ef9a7f4d41a42927b2e352cbb558791a4007Klaus Luettich implemented only atomic subtyping
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian MaederWeak amalgamation analysis?
f157913a0128ce772d0acd5038f61a7a619fd707Till MossakowskiInstantiate Transformation Application system for HasCASL?
f157913a0128ce772d0acd5038f61a7a619fd707Till MossakowskiAutomatic generation of Haskell (for a HasCASL subset)
f157913a0128ce772d0acd5038f61a7a619fd707Till MossakowskiProofs in HasCASL
87268d03b727bc9091716644fcf4048379accf02Till Mossakowski************************************************
87268d03b727bc9091716644fcf4048379accf02Till Mossakowski************************************************
aa6f6fa09091e92016598584162b9ba909af48ccTill MossakowskiConnecting Hets with MathServ
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski - haifa (http://www.dcs.shef.ac.uk/~simonf/HAIFA.html)
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski pros: * relies not on external tool
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski * light weight call
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till Mossakowski cons: * code is not well maintained
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till Mossakowski * a lot of the deserialization of the answer must be done
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till Mossakowski - call a java program included in MathServ distrib
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till Mossakowski pros: * works imediately
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till Mossakowski * deserilisation is mostly done in java
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till Mossakowski cons: * use of external tool
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till Mossakowski Use modified dfg2tptp to translate SPASS theories into TPTP problems
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till Mossakowski (ask Klaus for sources)
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till Mossakowski Add possibility to choose a prover out of a list of available provers
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski (similar to "More fine grained..." and behind more fine grained)
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski Adapt Comorphisms.KnownProvers to select a certain prover at the end of a
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till Mossakowski comorphism automatically
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maeder Adapt existing SPASS GUI to cover call of the MathServ broker
aa59f99fc45148fde3813cc560a5d3ebae6641aaTill Mossakowski by - transforming the grid layout packer into the packer
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski used in GUI.ProofManagement (easier to maintain and to extend)
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski - abstraction of certain parts of the GUI into helper functions
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski forms a new generic Prover-GUI toolkit
ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich - on top of this GUI toolkit
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski Write a GUI based on the generic Prover-GUI
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till Mossakowski to call MathServ's Vampire service directly
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till Mossakowski with additional parameters
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski************************************************
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski************************************************
69b043b647fa86377c06a8c413c8539f099d8084Till MossakowskiTranslation between Achim's ontology data structure and CASL (in Hets)
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskivisualization of "taxonomy" of CASL signatures
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski (subsorts = inheritance, unary preds = concepts, binary preds = relations)
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski last two ... partially done
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maederallgemeine Hets-GUI
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski f�r Anzeige von (un)bewiesenen Goals, ... done
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski bewiesene Goals als Axioms mit ausgeben ... was ist das ???
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill MossakowskiRecognize guarded fragment of CASL:
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski G ::= forall x . At(x) => G where At is a conjunction of atoms
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski | exists x . At(x) /\ G
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill MossakowskiJoost Visser wg. ATerms in Haskell => neues Repository
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
677a642991937d4bcf24dd30ef54328a9197fc86Till MossakowskiBeweise in Isabelle
69b043b647fa86377c06a8c413c8539f099d8084Till MossakowskiCASL consistency checker
180139f7c23c592aa6d4fe82ea5d15832ed25a84Till MossakowskiWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski (Vorbild: Larch-Handbuch)
677a642991937d4bcf24dd30ef54328a9197fc86Till MossakowskiSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
677a642991937d4bcf24dd30ef54328a9197fc86Till MossakowskiParser and static analysis for CSP-CASL
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski************************************************
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski************************************************
677a642991937d4bcf24dd30ef54328a9197fc86Till MossakowskiCASL consistency checker
677a642991937d4bcf24dd30ef54328a9197fc86Till MossakowskiIsaWin: support CASL-libraries
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maeder************************************************
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill MossakowskiRegulate concurrent proving
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski.dg files: store only current library; import .dg files for other libraries
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill MossakowskiIsabelle: use meta-quantifiers
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskilocal subsumption ?
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskibetter syntax (Tina)
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskicheck for proved theorems
420440d8d1a274241aae513044f0f9a0bc691985Christian MaederAbstractGraphView: switch to Result monad
420440d8d1a274241aae513044f0f9a0bc691985Christian Maederunite or rename consCheck and cons_checkers
420440d8d1a274241aae513044f0f9a0bc691985Christian MaederBinInt.casl: revealing in Int1 does not work correctly
420440d8d1a274241aae513044f0f9a0bc691985Christian Maederfrom Stefan W�lfl:
420440d8d1a274241aae513044f0f9a0bc691985Christian MaedercomputeTheory does not work across library imports
420440d8d1a274241aae513044f0f9a0bc691985Christian Maederlocal theorems
420440d8d1a274241aae513044f0f9a0bc691985Christian Maederall nodes named
420440d8d1a274241aae513044f0f9a0bc691985Christian Maederhierarchical Isabelle theories
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskidaVinci printing is not adequate
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskihiding of internal nodes does not work
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiFOL without quantifiers and with uniform disjunctions
b303a3717d229b102bca29e58d9e38c2f91fd233Christian Maeder (i.e. x R1 y \/ x R2 y)
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski (with and without =)
6c82551a9e6a38aa7c774db95ee957379f03df75Christian Maederalgorithmic path consistency over a relation algebra
6c82551a9e6a38aa7c774db95ee957379f03df75Christian Maeder plug in reasoner for this
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski develop correctness results (algorithmic path consistency=path consistency)
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiCASL sublogics:
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski---------------
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiFOL without quantifiers (with and without =)
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskiguarded fragment
963fd654abe69959032e5747732ec1c2f8fc9b41Till Mossakowski[from DOLCE cooperation:
9a9a05b15ab416d7d84fdb9115023e9136666304Till Mossakowskiontology mediation via pushouts/pullbacks/pulations
9a9a05b15ab416d7d84fdb9115023e9136666304Till MossakowskiRobinson consistency with shared theory constructed via pre-image?
963fd654abe69959032e5747732ec1c2f8fc9b41Till Mossakowskishow theorem links between same instances of different parameterized
963fd654abe69959032e5747732ec1c2f8fc9b41Till Mossakowski specs (where one is an extension of the other one)
963fd654abe69959032e5747732ec1c2f8fc9b41Till Mossakowskilink menu for %implies, $def, %cons, even without open proof obligation
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maederfor a proved theorem, show minimal part of DG needed for proof
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maedercons, def, mono for nodes
0317c2ef1c222f6664e9b494d10c68ee2114475eTill MossakowskiIsabelle interface: each qed should write proof info into file
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowskiglobally display nodes containing symbols mapped "twice" (i.e. via
581d3200cf7b4d344ae1ef0c581895723e2d527bChristian Maeder different signature morphisms)
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski and add a menu for each node allowing for tracking the different
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskitopsort coding: partial functions as relations?
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskitheorem link menu for proof obligations
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiUserManual/Chapter7.casl: local thm link starting from Monoid leads to type error
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowskiin Isabelle. Reason: Inlineaxioms does not translate ga_totality axioms
cb1c5be39138fb8f037dbefc121fe41adc06845dTill MossakowskiBuffer.het, sublogic of node Buffer:
cb1c5be39138fb8f037dbefc121fe41adc06845dTill MossakowskiFail: illegal node type in sublogic computation
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiJ�rgen Zimmer, Saarbr�cken+Edinburgh, Beweiserkennung f�r versch. Logiken im MathWeb
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskifor CSP-CASL example: with logic
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiheterogeneous static ana
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskitheorem links between nodes in different libraries
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian MaederbasicProofs: use info about used axioms
198093ec9afd8b459087dc30c94347bb7eeaa282Till Mossakowski ensure that axiom/thm names are unique
198093ec9afd8b459087dc30c94347bb7eeaa282Till MossakowskiOverload / inlineAxioms: injections
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maederremove "prove" menu in abstracted dg
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maederbetter sublogic analysis in codings
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maederthy files in subdir
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskiadjust path for thy files, such that hets can also be started from subdirs
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian MaederRestrict Sonjas simplifications to HasCASL
9565b030a2f09eeaac049389e27aa0977212a231Christian Maederadd suitable axioms to simplifier and CR
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian MaedercomputeTheory: remove double axioms
331ed72b03dc966e023fecae5f0116b119082ccdTill Mossakowskiadd suitable axioms to simplifier and classical reasoner
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowskibetter display of internal nodes (use tooltip?)
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowskiupdate Hets, CASL, daVinci on web page
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill MossakowskiCASL2PCFOL: x_i -> t_i, t=[inj(x_i)] (and what not!)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskipacking of binaries: add hets-update, refer to TclTk
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskitest for sublogic before applying comorphism
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMissing points for heterogeneous WADT 04 example:
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder- coding to Isabelle: translate sort gen constraints
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- Improve adapation to Isabelle's lexis
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIsabelle: (ask Christoph)
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski remove datatypes from sort list
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski prove local thm link (=> green)
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski "prove" menu with choice windows
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski incorporate sublogics
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski sublogic translation table
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski better interaction between Isabelle instance (for one node)
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski + selection of single goals that are proved
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski => use PGIP interface (Christoph, David)
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski correct show theory
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Keep proofs and lemmas in .thy files (kind of merge)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski CASL-like syntax
8fc331ee1cdf4cd55315ce5f31ed471f0dc7c9d6Klaus Luettich CASL annotation for lemmas that should be used in proof
8fc331ee1cdf4cd55315ce5f31ed471f0dc7c9d6Klaus Luettich inherit CASL's mixfix syntax
8fc331ee1cdf4cd55315ce5f31ed471f0dc7c9d6Klaus LuettichSignatures versus theories: where to store additional infos?
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maedercomp(id,x)=x for comorphism names
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian MaederGeneralise CASL2Modal
11cff49cc1e53960c6c83d88b841386ddbfedb0cKlaus LuettichMixfix analysis + typecheck for modality axiomatizations
11cff49cc1e53960c6c83d88b841386ddbfedb0cKlaus LuettichModal logics: modal logic, temporal logic, mu calculus
11cff49cc1e53960c6c83d88b841386ddbfedb0cKlaus Luettich+ translations (e.g. modal to FOL)
8fc331ee1cdf4cd55315ce5f31ed471f0dc7c9d6Klaus LuettichCASL->Haskell with free DTs (mark sortgens) + recursion
8fc331ee1cdf4cd55315ce5f31ed471f0dc7c9d6Klaus Luettich- List[Dec] wird List[Pos]
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maeder- node numbers do not match
d70b75218d4ab3cd49b29274f8a2844ad3b11634Klaus Luettich- thm links with external target should be provable as well
11cff49cc1e53960c6c83d88b841386ddbfedb0cKlaus LuettichRemove warnings
11cff49cc1e53960c6c83d88b841386ddbfedb0cKlaus LuettichDifferent types of logic translations
b67e71cf6027b5e8ef97e91e5e2e06ef84460e5bKlaus LuettichImprove Static analysis of structured specs
b67e71cf6027b5e8ef97e91e5e2e06ef84460e5bKlaus LuettichDevelopment graph calculus, Strategies for DG rules
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichManagement of change
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichIntegrate provers
aa6f6fa09091e92016598584162b9ba909af48ccTill Mossakowski Otter model checker
ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich FOL-prover by Uli Furhbach
ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich Isabelle codings: www.inf.ethz.ch/~vigano
ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich Renate Schmidt, Manchester: uses FOL prover for description logic
ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich (as efficient as DL-specific tools!)
ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich Look at PROSPER toolkit
ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich consistency: see IJCAR-workshop on non-provability in Cork
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maeder IJCAR workshop about logical frameworks and meta-languages
e0eee2b8144337bb54feb78d5a8b043041c9e028Till MossakowskiKlaus' wayfinding example
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowskiask Detlef: critical pairs, Fossacs paper by Francesco
e0eee2b8144337bb54feb78d5a8b043041c9e028Till MossakowskiUniForM workbench:
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowskifirst steps towards CASL instance, using ATerms and re-using MMISS instance
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowskivariants for specs (needed for DOLCE: CASL variant, DL variant, ...)
e0eee2b8144337bb54feb78d5a8b043041c9e028Till MossakowskiIntegration of MAYA and Isabelle/HOL (global HOL-Coding of
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski Grothendieck logic)
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski + for TAS: reflection of HOL in HOL, to be composed with encodings
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski (i.e. signatures, axioms, signature morphisms in HOL,
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski re-use ML signatures) (Einar)
e0eee2b8144337bb54feb78d5a8b043041c9e028Till MossakowskiDisplay Specs as daVinci subgraphs
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiUser interface
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski--------------
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiLogic graph window
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichInput text window
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichDevelopment graph window
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichProver windows
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHets interactive (provide cmd line interface, but hold loaded libraries in memory, provide switch to context of spec, and type checking of expressions, interaction with emacs mode)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPackaging of installation
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiGUI (vgl. VSE)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski with Eclipse, WXHaskell or GTk?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski how to integrate with event system of UniForM workbench?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiintegrate graphviz (or use Java interface for racer? or Isabelle browser? or...?)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski this interacts with GUI!
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian MaederData.Serizable (only when ghc supports it) better: rely on pointer equality
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiincrease performance
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiintegrate QuickCheck: come to lecture!
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski++++++++++++++++++++++++++++++++++++++++++++++++
180139f7c23c592aa6d4fe82ea5d15832ed25a84Till MossakowskiRemaining things
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski++++++++++++++++++++++++++++++++++++++++++++++++
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Coq, PTT in Maude
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till MossakowskiProofs with basic datatypes
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till MossakowskiVerbesserung der Fehlermeldungen
a07199a5d9c421ae4577a6fbbe3ebab5d7d68e82Klaus LuettichImprove encoding: CATS/basic_encode.sml (3 days)
a07199a5d9c421ae4577a6fbbe3ebab5d7d68e82Klaus LuettichMore HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
a07199a5d9c421ae4577a6fbbe3ebab5d7d68e82Klaus LuettichRenamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)
a07199a5d9c421ae4577a6fbbe3ebab5d7d68e82Klaus LuettichExample of Agnes und Frank: proofs in HOL-CASL (2 days)
a07199a5d9c421ae4577a6fbbe3ebab5d7d68e82Klaus LuettichTerm input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
a07199a5d9c421ae4577a6fbbe3ebab5d7d68e82Klaus LuettichExamples for cond rewriting -> Christophe
a07199a5d9c421ae4577a6fbbe3ebab5d7d68e82Klaus LuettichDoku: VSE-Prover, VSE-Method VSE-demo in Bremen?
fd8cfa293b960c770f15757e24fe5394d74671e2Till MossakowskiAdapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
fd8cfa293b960c770f15757e24fe5394d74671e2Till MossakowskiEigene IsaWin-Instanz mit CASL-RS statt HOL-RS
aa59f99fc45148fde3813cc560a5d3ebae6641aaTill MossakowskiHOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill MossakowskiHOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till MossakowskiHOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till MossakowskiEncoding of structured free (3 days)
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till MossakowskiEncoding of structured cofree (2 weeks)
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till MossakowskiEingabesyntax als Mix zwischen CASL und HOL (3 days)
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till MossakowskiAdapt Isabelle unions to CASL unions (1 week)
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till MossakowskiIsaWin git/src/isa_ext/casl_thy.sml (1 week)
ce507cba25d24cfbb7c13f51bd67c4462862c2d1Till MossakowskiGenerate Proof obligations (1 week)
ce507cba25d24cfbb7c13f51bd67c4462862c2d1Till MossakowskiAdd renaming to Isabelle kernel (2 months)
42e6f81f0794a7b6bc8e29e97c55668abe96da59Till MossakowskiRepository mit korrekten und fehlerhaften Specs
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till MossakowskiHetCATS User manual, Doku fuer Environments (2 weeks)
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till MossakowskiConversion ASF/SDF-Parser -> abstract syntax (in Haskell)
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till MossakowskiComparsion of parsers (ML-yacc parser, SDF-Parser)
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till MossakowskiConversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till MossakowskiPVS anbinden (Kooperation mit Cachan?)
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till MossakowskiPortations: Intel-Solaris, Mac OS-10 (2 weeks)
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowski(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm
ec75b50a89aea0d96fd19ce864225267d0625f25Till MossakowskiViews on CASL specs: CATS/viewer.sml (2 weeks)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiUebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiModule graph CATS/module_graph.sml (1 week) -> Maya?
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiATerms via XML: CATS/aterms.sml (2 weeks)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiNeues Tool-Schaubild auf Web-Seiten ver�ffentlichen
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiLibrary management: CATS/lib_ana.sml (2 weeks)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiVersion management/Uniform Workbench: CATS/lib_ana.sml (2 months)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski{- This does not work due to needed ordering:
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskiinstance Functor Set where
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski fmap = mapSet
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskiinstance Monad Set where
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski return = unitSet
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski m >>= k = unionManySets (setToList (fmap k m))
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiAufbau von comptable
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski--------------------
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski[("normal","normal","normal"),
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski ("normal","inclusion","normal"),
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski ("inclusion","normal","normal"),
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski ("inclusion","inclusion","inclusion")]
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiAufbau von ginfo
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski--------------------
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiMit initgraphs erzeugen
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiAufbau des Graphen selbst
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski------------------------