todo revision ead55e5013b301de3b72a254a9fb347ae04ba0a4
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
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
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/HiWi zu erledigen:
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till MossakowskiRepr�sentation �ndern:
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowski Beweisobjekte an DGs, nicht an Regeln -- done
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowski F�r Theoreme in Theorien an Beweisobjekte -- done
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowski BasicProof mit Liste von Beweisobjekten -- �berfl�ssig
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowski Definitionen auszeichnen -- done
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowski F�r alles siehe G_theory, ThSens und SenStatus.
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski Isabelles Beweisobjekte einbinden
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
0e3db835d379ceb594b0daa25a0590abb755a1acTill MossakowskiIntegration with PGIP
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski Hets needs to be equipped with a command-line interface that reads in
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski specification libraries and proof commands
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski Proof commands are special annotations in the libraries
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski All menu commands of the development graph interface (GUI/...) should become (proof) commands
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski when stepping through the specs, dg calculus generates proof obligations
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski (for the current dg node only),
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski which then can be discharged by Isabelle, SPASS etc.
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski That is, the proof commands always occur at the position in the text
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski that generates the dg node?!? or should they occur after each specification?
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski needs incremental parsing and static analysis for Hets libraries
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski easy: parse and analyse one specification at a time, and then process it with proof commands
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski more challenging: incrementally parse and analyse also individual specifications
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
0e3db835d379ceb594b0daa25a0590abb755a1acTill MossakowskiModal-CASL <-> CASL-DL
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski see Chapter 4 of "The Description Logic Handbook"
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski and ask Klaus for a print out of it
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowskiimprove Modal-CASL
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski possibly also modal logic in CoCASL
e2143dde7e5adcc35f1587e94c9279d8cbe3cbd5Till Mossakowski**************** task A ************************
e2143dde7e5adcc35f1587e94c9279d8cbe3cbd5Till MossakowskiProofs with Isabelle and SPASS
e2143dde7e5adcc35f1587e94c9279d8cbe3cbd5Till MossakowskiCASL basic datatypes
e2143dde7e5adcc35f1587e94c9279d8cbe3cbd5Till MossakowskiHasCASL examples
4a573a1ca4f8556b77e3467e6c2b261ba03e3036Till Mossakowski- improve simplifier for partiality in Isabelle coding
4a573a1ca4f8556b77e3467e6c2b261ba03e3036Till Mossakowski program interaction between solver, subgoaler and simplifier in such a way
4a573a1ca4f8556b77e3467e6c2b261ba03e3036Till Mossakowski that proofs of definedness conditions are postponed
db373255bd95ce4de47dde876c3a3bfc49c22a97Till Mossakowski************************************************
566b6a416bde2bc90d3aece2d992127303fb5d75Till MossakowskiFlorian (Till)
db373255bd95ce4de47dde876c3a3bfc49c22a97Till Mossakowski************************************************
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian MossakowskiModelchecker f�r algebraische Eigenschaften
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowski neue Hets-Option daf�r (Christian Maeder fragen)
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowski hets -n NonAssocRelationAlgebra --model datei.lisp Calculi/Algebra/RelationAlgebra.casl
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowski Datenstruktur zerlegen, siehe
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowski http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/debugging_e.htm
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowski siehe auch CASL.CompositionTable.ComputeTable
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowski Pr�fung der G�ltigkeit von CASL-Formel in einer Table, rekursiv:
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowski Allquantoren --> all, Existenzquantor --> any
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowski CASL-Junktoren --> Haskell-Junktoren
48fe12a47459e2cd54660d5d850e7aafadd6d77fFlorian Mossakowski Terme rekursiv auswerten, Operationen aus der Table nehmen
fd8cfa293b960c770f15757e24fe5394d74671e2Till MossakowskiAufgabe von Shi Hui: XML-Anfragen mit DCC-Ausdr�cken an Bremer Solver schicken
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski - ggf. Server nutzen
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski - Vorverarbeitung f�r Solver (z.B. Duplikate raus)
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski - Shi soll auf Freiburger XML-Format umsteigen (ggf. mit XSLT)
fd8cfa293b960c770f15757e24fe5394d74671e2Till MossakowskiApplikation1 ---
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski | | -- Freibuger Solver
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski XML --- |---- Franz�sischer Solver
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski | |-- Hets -- Bremer Solver
fd8cfa293b960c770f15757e24fe5394d74671e2Till MossakowskiApplikation2 ----- |
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski ConstraintCASL
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski Semantische Modelle/Korrektheit (CASL, HAsCASL)
fd8cfa293b960c770f15757e24fe5394d74671e2Till MossakowskiXML-Einlesen in Haskell:
fd8cfa293b960c770f15757e24fe5394d74671e2Till MossakowskiHXT (siehe OMDoc.XmlHandling): kann Namespaces
fd8cfa293b960c770f15757e24fe5394d74671e2Till Mossakowski(HaXML: kann Haskell-Datenypen in DTDs umwandeln)
fd8cfa293b960c770f15757e24fe5394d74671e2Till MossakowskiOutline der Diplomarbeit
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski Qualitative Constraint-Kalk�le (siehe Thomas)
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski CASL (siehe Paper T. Mossakowski: Relating CASL with Other Specification Languages:
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski the Institution Level Theoretical Computer Science 286, p. 367-475, 2002.)
36e567ca4ae0eabbfc918b98b96762b5cf07bbb8Till Mossakowski CASL-Formeln nur ganz kurz
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski ConstraintCASL
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski Signaturen, Signaturmorphismen (aus CASL)
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski Modelle (aus CASL)
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski Erf�lltheit von Formeln
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski optional: Erf�lltheitsbedingung
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski M |= sigma(phi) <=> M|_sigma |= phi
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski f�r Signaturmorphismus sigma:Sigma_1->Sigma_2
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski M \in Mod(Sigma_2), phi\in Sen(Sigma_1)
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski Formalisierung von Kalk�len in ConstraintCASL
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski Constraint-Solver (auch in ihren Eigenheiten)
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski �bersetzungen zwischen den verschieden Formaten
7d201e2dbe9872cdad86766bf65af57f3b9ab0aaTill Mossakowski praktischer Vergleich
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski�bersetzungen bis 30.Juni
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski ConstraintCASL -> Bremer Solver
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski Bremer Solver -> ConstraintCASL
3c8c05dc3358d217513d8e0e8e32ccd3e4947c05Florian Mossakowski Parser (mit Parsec), der Kompositionstabelle des Bremer Solvers
3c8c05dc3358d217513d8e0e8e32ccd3e4947c05Florian Mossakowski parsiert und ConstraintCASL-Spec (abstrakte Syntax) zur�ckgibt
3c8c05dc3358d217513d8e0e8e32ccd3e4947c05Florian Mossakowski Das kann das als Option in Hets eingebunden werden (Christian Maeder)
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill MossakowskiFreiburger Constraint-Solver angucken im Juli
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski�bersetzungen bis 31. Juli
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski ConstraintCASL -> Freibuger Solver/XML-Format
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski Freibuger Solver/XML-Format -> ConstraintCASL
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski************************************************
677a642991937d4bcf24dd30ef54328a9197fc86Till MossakowskiHendrik (Till)
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski************************************************
198093ec9afd8b459087dc30c94347bb7eeaa282Till Mossakowskiwerden Signatur-Symbole in OMDoc mit der Theorie versehen, in der
198093ec9afd8b459087dc30c94347bb7eeaa282Till Mossakowski sie als erstes eingef�hrt wurden?
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till Mossakowski checken f�r Library-Importe
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till MossakowskiOMDoc/OpenMath-Formeln als Haskell-Datentyp formulieren; diesen als Zwischendatentyp verwenden
677a642991937d4bcf24dd30ef54328a9197fc86Till MossakowskiHiding: unterschiedlich in OMDoc und Hets
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maederein Hets-Hiding-Link mit einer Inklusion Sigma_1->Sigma_2 als
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski Signaturmorphismus
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski wird �bersetzt in einen OMDoc-Theoriemorphismus
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski mit leerer/identischer Abbildung, bei dem die Symbole aus
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski Sigma_2 \ Sigma_1 versteckt werden
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski Wenn der Signaturmorphismus keine Inklusion ist, ist keine
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski �bersetzung m�glich -> Fehler
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowskiein OMDoc-Theoriemorphismus mit Hiding, der eine Inklusion ist
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski (also leere bzw. identische Abbildung) wird �bersetzt
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski in einen Hets-Hiding-Link, mit Inklusion als Signaturmorphismus
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski falls der OMDoc-Theoriemorphismus keine Inklusion ist, muss
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski ein Hets-Hiding-Link, gefolgt von einem normalen (globalen) Link,
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski der dann die Umbenennung macht, erzeugt werden
677a642991937d4bcf24dd30ef54328a9197fc86Till MossakowskiLogiken: �ber verschiedene OMDoc-Theorien mit URI
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski- CASL-Logik: "Relating CASL with other specification languages", S.401-408
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski- Konservative, definitionale und monomorphe Erweiterungen, Konsistenz
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski siehe CASL reference manual (suche nach conservative)
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski- warum sind konservative Erweiterungen wichtig?
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski - um zu pr�fen, ob Spezifikationen konsistent sind, also implementiert
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski werden k�nnen
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski - f�r Refinement-Beweise
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski- Algorithmen zur Pr�fung von Erweiterungen, ob diese konservativ,
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski definitional oder monomorph sind
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski - Beschreibung des Algorithmus in Pseudocode
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski - Korrektheitsbeweis, d.h. f�r die Erweiterungen, die der Algorithmus
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski als konservativ erkennt, muss f�r jedes Modell der kleineren
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski Spezifikation eine Modellerweiterung zur gr��eren Spezifikation
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski gefunden werden. Z.B. im Falle von free types kann dies eine
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski Termalgebra-Konstruktion sein.
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski SP1 -- \sigma --> SP2
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski konservativ: jedes SP_1-Modell M1 hat eine Erweiterung zu einem
b04658442a4419349d41c931f2a3bda49e8be9e8Till Mossakowski SP2-Modell M2 mit M2|_\sigma=M1.
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowskiport CCC to Haskell
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian MaederFunktionen 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"
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maedercheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskicheck' [] = ([([],[])],emptyUniqSet)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maedercheck' [EqnInfo n ctx ps (MatchResult CanFail _)]
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskicheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski | all_vars ps = (pats, addOneToUniqSet indexs n)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski (pats,indexs) = check' rs
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski-- falls ein Konstruktor dabei ist: split_by_constructor
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maedercheck' qs@((EqnInfo n ctx ps result):_)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski | all_vars ps = ([], unitUniqSet n)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski | constructors = split_by_constructor qs
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski | only_vars = first_column_only_vars qs
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski | otherwise = panic "Check.check': Not implemented :-("
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski -- Note: RecPats will have been simplified to ConPats
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski -- at this stage.
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski constructors = or (map is_con qs)
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maeder only_vars = and (map is_var qs)
a1bb9f8f9143aa2d84dfab69ed988d94f7e3b196Till Mossakowskisubsort definitions: are conservative if formula is satisfiable
a1bb9f8f9143aa2d84dfab69ed988d94f7e3b196Till Mossakowski (generate proof obligation)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
e1f2ef9a7f4d41a42927b2e352cbb558791a4007Klaus LuettichOWL-DL (<)-> CASL-DL
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski highlight does not work properly for HasCASL/Set.het or UserManual/Sbcs.casl
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski some operation symbols
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski show hets output immediately
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski C-c C-g for hets -g
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski when hets terminates abnormally (e.g. with a fail), emacs loops
87268d03b727bc9091716644fcf4048379accf02Till Mossakowski C-n jumps to the next error, but the message windows is not always scrolled
87268d03b727bc9091716644fcf4048379accf02Till Mossakowski in such a way that the error is at the top (for long error lists)
87268d03b727bc9091716644fcf4048379accf02Till Mossakowski Version for XEamcs?
1604c7123ebd603b2ca3eb6d2bd325cbdb23ee99Till Mossakowski should work with parser error messages as well (adapt these?)
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski************************************************
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski************************************************
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till Mossakowskilook at command line interface (just call hets)
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till Mossakowskiimplement simplified rule Theorem-Hide-Shift
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till Mossakowskitry out examples
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till Mossakowskiconservativity calculus
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till Mossakowskiweakly amalgamable cocones
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till Mossakowskidevelopment graph calculus
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till Mossakowski(see Sect. IV:4.4 of the CASL Reference Manual)
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowskilook at Proofs/EdgeUtils.hs Proofs/StatusUtils.hs Proofs/Global.hs
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till Mossakowskitest command line interface (just call hets)
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maedertest development graph GUI:
aa59f99fc45148fde3813cc560a5d3ebae6641aaTill Mossakowski global decomposition
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski menu edit - unnamed nodes - hide/show nodes,
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski node menu: show just subtree / undo
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski interaction with edit - proofs - automatic?
ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich use update of uDrawGraph-nodes,edges instead of erasing and adding nodes
ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich for attribute changes like color
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till Mossakowskiprofiling for "automatic" (look at www.haskell.org/ghc)
aa59f99fc45148fde3813cc560a5d3ebae6641aaTill Mossakowskirestrict proofs: only one prove window per node at a given time
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskifurther task 1
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskifurther task 2
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian MaederUni-Refactoring,
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskimake modules hierarchical, change scoped type variables for ghc-6.5
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski(and older ghcs), replace deprecated code (i.e. FiniteMap, hslibs),
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskiuse HaXml as a cabalized library, provide uni as (one?) cabal
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskipackage(s), uni used to work under windows as well, watch the
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskii.e. FilePath, Process discussions (libraries@haskell.org)
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskipossibly switch to a subversion repository, talk to Achim
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski(amahnke@tzi.de)
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskifurther task 3
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowskichange management
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski reload button im Edit-Men� hinzuf�gen (GUI/ConvertAbstractToDevgraph.hs)
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski reload macht folgendes:
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski lade CASL-Datei neu ==> neuer Entwicklungsgraph
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski vergleiche alten+neuen Entwicklungsgraph, konstruiere eine
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski Abbildung (Common/Lib/Map.hs) von alt nach neu
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski (jeweils eine Abblidung f�r Knoten und eine f�r Kanten)
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski Kriterien f�r Finden der Knotenabbildung:
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maedereinfaches Merge von lokalen Beweisen eines abgespeichteren DG
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski in aktuellen DG
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskifurther task 4
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskigraph of Haskell module dependencies
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski using .import files
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskifurther task 5
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder************************************************
180139f7c23c592aa6d4fe82ea5d15832ed25a84Till Mossakowskiport hets to windows. -- costs too much energy at this stage! Till
420440d8d1a274241aae513044f0f9a0bc691985Christian MaederIf hets should become successful then requests for support under
420440d8d1a274241aae513044f0f9a0bc691985Christian Maederwindows will surely follow.
420440d8d1a274241aae513044f0f9a0bc691985Christian MaederGhc, uni and uDrawGraph should work under windows. Only Isabelle does
420440d8d1a274241aae513044f0f9a0bc691985Christian Maedernot exist for windows, but SPASS does. Probably only a few path
420440d8d1a274241aae513044f0f9a0bc691985Christian Maedercomputations need to be adapted (made modular) within hets. Also
420440d8d1a274241aae513044f0f9a0bc691985Christian Maederposition computations (of Parsec) should be checked under windows.
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskifurther task 6
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski************************************************
6c82551a9e6a38aa7c774db95ee957379f03df75Christian Maederrefactor pretty printing
b303a3717d229b102bca29e58d9e38c2f91fd233Christian Maedereine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowskiund andere Formate besser zu unterst�tzen und einheitlichen PP code
6c82551a9e6a38aa7c774db95ee957379f03df75Christian Maeder(independent from GlobalAnnos) f�r die (Het-)CASL (and HasCASL!)
6c82551a9e6a38aa7c774db95ee957379f03df75Christian MaederDatentypen (particularly for HasCASL data types) zu bekommen.
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiLaTeX: see listings.sty for LaTeX generation (cf. CoSiT paper)
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski************************************************
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskiremaining stuff
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski************************************************
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maederset up a ticket and tracking systems (for bugs and features) instead
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maederof this messy todo list
963fd654abe69959032e5747732ec1c2f8fc9b41Till Mossakowski--> sourceforge???
9a9a05b15ab416d7d84fdb9115023e9136666304Till Mossakowskirefactoring of dgraphs: add unique tags + hashes (but no table)
9a9a05b15ab416d7d84fdb9115023e9136666304Till Mossakowski how to compare complex datastructures:
9a9a05b15ab416d7d84fdb9115023e9136666304Till Mossakowski tag x1==tag x2 || (hash x1==hash x2 && x1==x2)
963fd654abe69959032e5747732ec1c2f8fc9b41Till Mossakowskidisplay library graph
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maederunify GUI/AbstractGraphView.hs and Taxonomy/AbstractGraphView.hs
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowskiand uni/appl/ontologytool/AbstractGraphView.hs
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowski(make it really abstract), possibly contact amahnke@tzi.de regarding
581d3200cf7b4d344ae1ef0c581895723e2d527bChristian MaederTaxonomy, possibly use uni/appl/ontologytool instead of Taxonomy!
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskiset up default simplifier
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskiset up default tactics using axioms
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski (see DOLCE sample files)
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskiimprove efficiency (e.g. of UserManual/Sbcs.casl), using profiling
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski************************************************
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski************************************************
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowskigenerate infrastructure for circular coinduction
cb1c5be39138fb8f037dbefc121fe41adc06845dTill MossakowskiCCS example: commutativity of || by coinduction
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill MossakowskiIsabelle coding
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski- improve display syntax in HasCASL-Isabelle coding
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maeder- identifiers in mixfix templates must be excluded as ordinary
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maederidentifiers (i.e. as quantified variables)
198093ec9afd8b459087dc30c94347bb7eeaa282Till Mossakowskimore abstract datatypes?
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maedercollect the patches for programatica (or create a package)
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder- conv (SN i p) = PN i (S p)
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder+ conv (SN i p) = PN i (Sn (show i) p)
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maederin programatica/tools/base/parse2/NumberNames.hs
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maederfixes translation error of Pair
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskisimplification of HasCASL sentences (omit types)
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian MaederLogic COL is a ruin
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maederlogic coding from the comand line with printing of results
0d42a1490aa92c24b19823f745104eefbf29675dChristian MaederHaskell modules: hiding, renaming
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
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiStatic analysis for HasCASL
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maeder pattern analysis for program equations
96cc01853b72b9d0fdc9e3d309a196a2216de119Christian Maeder implemented only atomic subtyping
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian MaederWeak amalgamation analysis?
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian MaederInstantiate Transformation Application system for HasCASL?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAutomatic generation of Haskell (for a HasCASL subset)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiProofs in HasCASL
04ee0d20d16836bb6e835029a807c304973dea46Till MossakowskiCoding HasCASL -> Isabelle with definedness axioms
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski only strict functions are defined
04ee0d20d16836bb6e835029a807c304973dea46Till MossakowskiIsabelle interface
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski One emacs with spec and proof buffer
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski Reload button should rebuild buffers while keeping as much as possible
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski keep structuring of Hets theories
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
69b043b647fa86377c06a8c413c8539f099d8084Till MossakowskiRainer (Klaus)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
8fc331ee1cdf4cd55315ce5f31ed471f0dc7c9d6Klaus LuettichSPASS encoding improvements in SPASS.Conversions/Comorphisms.CASL2SPASS
8fc331ee1cdf4cd55315ce5f31ed471f0dc7c9d6Klaus Luettich - if there is only one sort in the signature eliminate it
8fc331ee1cdf4cd55315ce5f31ed471f0dc7c9d6Klaus Luettich special case: (freely) generated sorts are not eliminated
8fc331ee1cdf4cd55315ce5f31ed471f0dc7c9d6Klaus Luettich new flag in SPASS sign: singleSorted
8fc331ee1cdf4cd55315ce5f31ed471f0dc7c9d6Klaus Luettich Sentences are modified in CASL2SPASS
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maeder all variable declarations have to consider the flag
8fc331ee1cdf4cd55315ce5f31ed471f0dc7c9d6Klaus Luettich (quantified formulas) variable lists without types
11cff49cc1e53960c6c83d88b841386ddbfedb0cKlaus Luettich - F:Membership ==> true
11cff49cc1e53960c6c83d88b841386ddbfedb0cKlaus Luettich - T:Cast is omitted
11cff49cc1e53960c6c83d88b841386ddbfedb0cKlaus Luettich - T:Sorted_term is omitted
8fc331ee1cdf4cd55315ce5f31ed471f0dc7c9d6Klaus Luettich typings in the signature have to be removed in SPASS.Conversions
8fc331ee1cdf4cd55315ce5f31ed471f0dc7c9d6Klaus Luettich empty declarations list
d70b75218d4ab3cd49b29274f8a2844ad3b11634Klaus LuettichSPASS encoding improvements in CASL2SPASS
8fc331ee1cdf4cd55315ce5f31ed471f0dc7c9d6Klaus Luettich - if there are predicates defined upon equality substitute them with equality
d70b75218d4ab3cd49b29274f8a2844ad3b11634Klaus Luettich and remove them from the signature
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maeder find definitions (Equivalences) where one side is a binary predicate
d70b75218d4ab3cd49b29274f8a2844ad3b11634Klaus Luettich and the other side is a builtin equality application (Strong_equation)
d70b75218d4ab3cd49b29274f8a2844ad3b11634Klaus Luettich return the full qualified (with type) predicate(s)
d70b75218d4ab3cd49b29274f8a2844ad3b11634Klaus Luettich this is done before the translation of the signature/sentences happens
11cff49cc1e53960c6c83d88b841386ddbfedb0cKlaus Luettich remove eqPrediate symbols from signature
11cff49cc1e53960c6c83d88b841386ddbfedb0cKlaus Luettich substitute eqPredications with Strong_equation in the Formulas
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************
ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettichfor ProofManagement-GUI
ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich mark imported theorems for selection
ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich provide structured (based on spec-names) selection/deselection facility
ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich of axioms and theorems
ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettichtrace if liniarity of sentences along development is given
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maederfor consistency checking with Isabelle, look at the following SAT-Solvers:
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill MossakowskiMChaff, ZChaff, Berkmin
e0eee2b8144337bb54feb78d5a8b043041c9e028Till MossakowskiConsistency checker interface
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski via global interface, accessible from global and node menus
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maeder use falseSentence from Logic.Logic (property: holds in no model)
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski proved -> inconsistent
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski disproved -> consistent (assuming completeness)
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski batch mode for automatic provers such as SPASS
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski (use automatic flag for provers)
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowskibatch interface for Isabelle
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski each goal is proved separatedly, with a time limit enforced
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski by killing the process
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski the tactic is
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski "using Ax1 ... Axn by auto"
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski where Ax1 ... Axn is the list of all axioms.
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski "auto" could be replaced with "best", "blast" etc. (user selection)
e0eee2b8144337bb54feb78d5a8b043041c9e028Till MossakowskiIgnore axiom selection for interactive provers
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiTranslation between Achim's ontology data structure and CASL (in Hets)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskivisualization of "taxonomy" of CASL signatures
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (subsorts = inheritance, unary preds = concepts, binary preds = relations)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich last two ... partially done
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
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian MaederParser and static analysis for CSP-CASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCASL consistency checker
180139f7c23c592aa6d4fe82ea5d15832ed25a84Till MossakowskiIntegration with generic prover interface?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till Mossakowskienhance Web interface with SPASS (%implied, consistency)
ead55e5013b301de3b72a254a9fb347ae04ba0a4Till Mossakowskitranslation of proofs along comorphisms (it this necessary at all???)
a07199a5d9c421ae4577a6fbbe3ebab5d7d68e82Klaus Luettich use inverse morphism?
a07199a5d9c421ae4577a6fbbe3ebab5d7d68e82Klaus Luettich leads to translation of G_theory along comorphism that also
a07199a5d9c421ae4577a6fbbe3ebab5d7d68e82Klaus Luettich keeps proof status info
a07199a5d9c421ae4577a6fbbe3ebab5d7d68e82Klaus Luettich this may be used in GUI prover interfaces for recovering old proof attempts
a07199a5d9c421ae4577a6fbbe3ebab5d7d68e82Klaus Luettich and offering them as default
a07199a5d9c421ae4577a6fbbe3ebab5d7d68e82Klaus LuettichproveCMDLinteractive (PGIP)
fd8cfa293b960c770f15757e24fe5394d74671e2Till MossakowskiModel expansion flag for comorphisms
aa59f99fc45148fde3813cc560a5d3ebae6641aaTill MossakowskiUmlaute in daVinci anzeigen
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till MossakowskiFragen an Michael:
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till Mossakowskiwerden Links in der richtigen Reihenfolge geschrieben (S. 183 OMDoc)?
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till Mossakowski was ist dort eigentlich das Problem?
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till MossakowskiCodierung von Subsorten?
ce507cba25d24cfbb7c13f51bd67c4462862c2d1Till Mossakowskipaper with Paolo
ce507cba25d24cfbb7c13f51bd67c4462862c2d1Till Mossakowski semantic adequecy of HOL translation
42e6f81f0794a7b6bc8e29e97c55668abe96da59Till MossakowskiRegulate concurrent proving
42e6f81f0794a7b6bc8e29e97c55668abe96da59Till Mossakowski.dg files: store only current library; import .dg files for other libraries
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till MossakowskiIsabelle: use meta-quantifiers
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowskilocal subsumption ?
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowskibetter syntax (Tina)
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowskicheck for proved theorems
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till MossakowskiAbstractGraphView: switch to Result monad
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowskiunite or rename consCheck and cons_checkers
ec75b50a89aea0d96fd19ce864225267d0625f25Till MossakowskiBinInt.casl: revealing in Int1 does not work correctly
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskifrom Stefan W�lfl:
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskicomputeTheory does not work across library imports
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskilocal theorems
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskiall nodes named
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskihierarchical Isabelle theories
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskidaVinci printing is not adequate
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskihiding of internal nodes does not work
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiFOL without quantifiers and with uniform disjunctions
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski (i.e. x R1 y \/ x R2 y)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski (with and without =)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskialgorithmic path consistency over a relation algebra
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski plug in reasoner for this
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski develop correctness results (algorithmic path consistency=path consistency)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiCASL sublogics:
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski---------------
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiFOL without quantifiers (with and without =)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskiguarded fragment
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski[from DOLCE cooperation:
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskiontology mediation via pushouts/pullbacks/pulations
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiRobinson consistency with shared theory constructed via pre-image?
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskishow theorem links between same instances of different parameterized
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski specs (where one is an extension of the other one)
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskilink menu for %implies, $def, %cons, even without open proof obligation
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskifor a proved theorem, show minimal part of DG needed for proof
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskicons, def, mono for nodes
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiIsabelle interface: each qed should write proof info into file
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskiglobally display nodes containing symbols mapped "twice" (i.e. via
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski different signature morphisms)
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski and add a menu for each node allowing for tracking the different
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskitopsort coding: partial functions as relations?
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowskitheorem link menu for proof obligations
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian MaederUserManual/Chapter7.casl: local thm link starting from Monoid leads to type error
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowskiin Isabelle. Reason: Inlineaxioms does not translate ga_totality axioms
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till MossakowskiBuffer.het, sublogic of node Buffer:
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till MossakowskiFail: illegal node type in sublogic computation
21d72ad1e64e2fa6d831f9def45d6dc21f6e0bd8Till MossakowskiJ�rgen Zimmer, Saarbr�cken+Edinburgh, Beweiserkennung f�r versch. Logiken im MathWeb
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowskifor CSP-CASL example: with logic
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowskiheterogeneous static ana
601f11cf0b4164a6a718038a736ae3d579f3a27cTill Mossakowskitheorem links between nodes in different libraries
7ed2a775680fb1a29e6907d372124906b7746420Till MossakowskibasicProofs: use info about used axioms
7ed2a775680fb1a29e6907d372124906b7746420Till Mossakowski ensure that axiom/thm names are unique
8980a8c8137a3a4c69bf9fdb3eca5b4b7f6e69c9Till MossakowskiOverload / inlineAxioms: injections
85ab61b931e22a72a53628b8aa5d059eeaedf1bdTill Mossakowskiremove "prove" menu in abstracted dg
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskibetter sublogic analysis in codings
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskithy files in subdir
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskiadjust path for thy files, such that hets can also be started from subdirs
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiRestrict Sonjas simplifications to HasCASL
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskiadd suitable axioms to simplifier and CR
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskicomputeTheory: remove double axioms
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskiadd suitable axioms to simplifier and classical reasoner
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskibetter display of internal nodes (use tooltip?)
331ed72b03dc966e023fecae5f0116b119082ccdTill Mossakowskiupdate Hets, CASL, daVinci on web page
b2768faecd6610af357407a8ddfe1412a18f8ebcChristian MaederCASL2PCFOL: x_i -> t_i, t=[inj(x_i)] (and what not!)
950ecce40ed5a97adf4460be07b47e3a0d0b1e56Till Mossakowskipacking of binaries: add hets-update, refer to TclTk
3e2c4de10a0eb284938b5d5307d1c1fc2f799456Till Mossakowskitest for sublogic before applying comorphism
dedca4980b2d43bc343ffcaf73e0617524f9720cTill MossakowskiMissing points for heterogeneous WADT 04 example:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- coding to Isabelle: translate sort gen constraints
4be2c76af9603b48b147f1f369f713e78544974eTill Mossakowski- Improve adapation to Isabelle's lexis
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIsabelle: (ask Christoph)
331ed72b03dc966e023fecae5f0116b119082ccdTill Mossakowski remove datatypes from sort list
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski prove local thm link (=> green)
60082d649e5bbb1c54f73f8921c3c390170e6c46Till Mossakowski "prove" menu with choice windows
60082d649e5bbb1c54f73f8921c3c390170e6c46Till Mossakowski incorporate sublogics
60082d649e5bbb1c54f73f8921c3c390170e6c46Till Mossakowski sublogic translation table
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
2d76902bf3b380a32268ccc0d2cd9e376988a060Till MossakowskiGeneralise 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 MossakowskiCASL->Haskell with free DTs (mark sortgens) + recursion
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski- List[Dec] wird List[Pos]
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
198093ec9afd8b459087dc30c94347bb7eeaa282Till Mossakowski use graph grammars to model rules? transformation units?
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
31c49f2fa23d4ac089f35145d80a224deb6ea7e4Till Mossakowskiask Detlef: critical pairs, Fossacs paper by Francesco
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
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maeder (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************************************************
b172714c339053a40393dc0cf4f9151c97695e01Till 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)
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski with Eclipse, WXHaskell or GTk?
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski how to integrate with event system of UniForM workbench?
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskiintegrate graphviz (or use Java interface for racer? or Isabelle browser? or...?)
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski this interacts with GUI!
cc7492cd222f08d17c994912bcb0c60083ae2bc9Till MossakowskiData.Serizable (only when ghc supports it) better: rely on pointer equality
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiincrease performance
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskiintegrate QuickCheck: come to lecture!
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski++++++++++++++++++++++++++++++++++++++++++++++++
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRemaining things
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski++++++++++++++++++++++++++++++++++++++++++++++++
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Coq, PTT in Maude
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiProofs 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------------------------