Cross Reference: /hets/todo
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
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski************************************************
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till MossakowskiImmanuel
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 Mossakowski
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till MossakowskiBasicProof in Proofs.Proofs: sind Datenstrukturen f�r informelle Beweise OK?
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till MossakowskiKonfidenzgrade von Beweisen?
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski
9b6a240bf8a37887add38054413d7f880bd59cf3Till Mossakowskivon Till/HiWi zu erledigen:
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till MossakowskiRepr�sentation �ndern:
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski Beweisobjekte an DGs, nicht an Regeln -- done
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski F�r Theoreme in Theorien an Beweisobjekte -- done
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski BasicProof mit Liste von Beweisobjekten -- �berfl�ssig
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski Definitionen auszeichnen -- done
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski F�r alles siehe G_theory, ThSens und SenStatus.
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski Isabelles Beweisobjekte einbinden
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski
db373255bd95ce4de47dde876c3a3bfc49c22a97Till Mossakowski
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski************************************************
db373255bd95ce4de47dde876c3a3bfc49c22a97Till MossakowskiRazvan (Till)
db373255bd95ce4de47dde876c3a3bfc49c22a97Till Mossakowski************************************************
2b60e1b81de56782be899de982c0908696f3530dTill Mossakowski
566b6a416bde2bc90d3aece2d992127303fb5d75Till MossakowskiIntegration with PGIP
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski Hets needs to be equipped with a command-line interface that reads in
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski specification libraries and proof commands
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski Proof commands are special annotations in the libraries
2b60e1b81de56782be899de982c0908696f3530dTill Mossakowski All menu commands of the development graph interface (GUI/...) should become (proof) commands
2b60e1b81de56782be899de982c0908696f3530dTill Mossakowski when stepping through the specs, dg calculus generates proof obligations
2b60e1b81de56782be899de982c0908696f3530dTill Mossakowski (for the current dg node only),
2b60e1b81de56782be899de982c0908696f3530dTill Mossakowski which then can be discharged by Isabelle, SPASS etc.
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski That is, the proof commands always occur at the position in the text
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski that generates the dg node?!? or should they occur after each specification?
38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski needs incremental parsing and static analysis for Hets libraries
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski easy: parse and analyse one specification at a time, and then process it with proof commands
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski more challenging: incrementally parse and analyse also individual specifications
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski************************************************
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiAnton (Till)
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski************************************************
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiModal-CASL <-> CASL-DL
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski see Chapter 4 of "The Description Logic Handbook"
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski and ask Klaus for a print out of it
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowskiimprove Modal-CASL
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski possibly also modal logic in CoCASL
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski**************** task A ************************
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiProofs with Isabelle and SPASS
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiCASL basic datatypes
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiHasCASL examples
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski- improve simplifier for partiality in Isabelle coding
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski program interaction between solver, subgoaler and simplifier in such a way
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski that proofs of definedness conditions are postponed
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski************************************************
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiFlorian (Till)
2d6b942b2d10709143b699783f38957d8856e67fTill Mossakowski************************************************
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till Mossakowski
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till MossakowskiModelchecker f�r algebraische Eigenschaften
2d6b942b2d10709143b699783f38957d8856e67fTill Mossakowski neue Hets-Option daf�r (Christian Maeder fragen)
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till Mossakowski hets -n NonAssocRelationAlgebra --model datei.lisp Calculi/Algebra/RelationAlgebra.casl
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till Mossakowski Datenstruktur zerlegen, siehe
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/debugging_e.htm
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski siehe auch CASL.CompositionTable.ComputeTable
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski Pr�fung der G�ltigkeit von CASL-Formel in einer Table, rekursiv:
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski Allquantoren --> all, Existenzquantor --> any
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski CASL-Junktoren --> Haskell-Junktoren
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski Terme rekursiv auswerten, Operationen aus der Table nehmen
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski (siehe CASL.AS_CASL_Basic)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiAufgabe von Shi Hui: XML-Anfragen mit DCC-Ausdr�cken an Bremer Solver schicken
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski - ggf. Server nutzen
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski - Vorverarbeitung f�r Solver (z.B. Duplikate raus)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski - Shi soll auf Freiburger XML-Format umsteigen (ggf. mit XSLT)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiApplikation1 ---
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski | | -- Freibuger Solver
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski XML --- |---- Franz�sischer Solver
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski | |-- Hets -- Bremer Solver
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiApplikation2 ----- |
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski ConstraintCASL
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski |
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski Semantische Modelle/Korrektheit (CASL, HAsCASL)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiXML-Einlesen in Haskell:
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiHXT (siehe OMDoc.XmlHandling): kann Namespaces
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski(HaXML: kann Haskell-Datenypen in DTDs umwandeln)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiOutline der Diplomarbeit
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski Qualitative Constraint-Kalk�le (siehe Thomas)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski CASL (siehe Paper T. Mossakowski: Relating CASL with Other Specification Languages:
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski the Institution Level Theoretical Computer Science 286, p. 367-475, 2002.)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski CASL-Formeln nur ganz kurz
a1bb9f8f9143aa2d84dfab69ed988d94f7e3b196Till Mossakowski ConstraintCASL
a1bb9f8f9143aa2d84dfab69ed988d94f7e3b196Till Mossakowski Signaturen, Signaturmorphismen (aus CASL)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Modelle (aus CASL)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Formeln
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Erf�lltheit von Formeln
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski optional: Erf�lltheitsbedingung
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski M |= sigma(phi) <=> M|_sigma |= phi
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich f�r Signaturmorphismus sigma:Sigma_1->Sigma_2
e1f2ef9a7f4d41a42927b2e352cbb558791a4007Klaus Luettich M \in Mod(Sigma_2), phi\in Sen(Sigma_1)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski Formalisierung von Kalk�len in ConstraintCASL
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski Constraint-Solver (auch in ihren Eigenheiten)
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski �bersetzungen zwischen den verschieden Formaten
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski praktischer Vergleich
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski Anwendung
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski�bersetzungen bis 30.Juni
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski ConstraintCASL -> Bremer Solver
87268d03b727bc9091716644fcf4048379accf02Till Mossakowski CASL/ComputeTable
87268d03b727bc9091716644fcf4048379accf02Till Mossakowski Bremer Solver -> ConstraintCASL
87268d03b727bc9091716644fcf4048379accf02Till Mossakowski Parser (mit Parsec), der Kompositionstabelle des Bremer Solvers
87268d03b727bc9091716644fcf4048379accf02Till Mossakowski parsiert und ConstraintCASL-Spec (abstrakte Syntax) zur�ckgibt
1604c7123ebd603b2ca3eb6d2bd325cbdb23ee99Till Mossakowski Das kann das als Option in Hets eingebunden werden (Christian Maeder)
aa6f6fa09091e92016598584162b9ba909af48ccTill MossakowskiFreiburger Constraint-Solver angucken im Juli
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski�bersetzungen bis 31. Juli
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski ConstraintCASL -> Freibuger Solver/XML-Format
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski CASL/ComputeTable
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski Option: comptable.xml
e1f2ef9a7f4d41a42927b2e352cbb558791a4007Klaus Luettich Freibuger Solver/XML-Format -> ConstraintCASL
b021b399b59fb7009308ed7a3eda30182dea7976Klaus Luettich
b021b399b59fb7009308ed7a3eda30182dea7976Klaus Luettich************************************************
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiHendrik (Till)
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski************************************************
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskiwerden Signatur-Symbole in OMDoc mit der Theorie versehen, in der
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski sie als erstes eingef�hrt wurden?
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maeder checken f�r Library-Importe
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maeder
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian MaederOMDoc/OpenMath-Formeln als Haskell-Datentyp formulieren; diesen als Zwischendatentyp verwenden
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maeder
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian MaederHiding: unterschiedlich in OMDoc und Hets
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maederein Hets-Hiding-Link mit einer Inklusion Sigma_1->Sigma_2 als
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maeder Signaturmorphismus
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maeder wird �bersetzt in einen OMDoc-Theoriemorphismus
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maeder mit leerer/identischer Abbildung, bei dem die Symbole aus
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maeder Sigma_2 \ Sigma_1 versteckt werden
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maeder Wenn der Signaturmorphismus keine Inklusion ist, ist keine
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski �bersetzung m�glich -> Fehler
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskiein OMDoc-Theoriemorphismus mit Hiding, der eine Inklusion ist
e1f2ef9a7f4d41a42927b2e352cbb558791a4007Klaus Luettich (also leere bzw. identische Abbildung) wird �bersetzt
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski in einen Hets-Hiding-Link, mit Inklusion als Signaturmorphismus
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski falls der OMDoc-Theoriemorphismus keine Inklusion ist, muss
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till Mossakowski ein Hets-Hiding-Link, gefolgt von einem normalen (globalen) Link,
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till Mossakowski der dann die Umbenennung macht, erzeugt werden
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till Mossakowski
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till MossakowskiLogiken: �ber verschiedene OMDoc-Theorien mit URI
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till Mossakowski
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till Mossakowski
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till Mossakowski
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski************************************************
420440d8d1a274241aae513044f0f9a0bc691985Christian MaederMingyi (Till)
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder************************************************
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder
420440d8d1a274241aae513044f0f9a0bc691985Christian MaederDiplomarbeit
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder- CASL-Logik: "Relating CASL with other specification languages", S.401-408
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder- Konservative, definitionale und monomorphe Erweiterungen, Konsistenz
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder siehe CASL reference manual (suche nach conservative)
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder- warum sind konservative Erweiterungen wichtig?
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder - um zu pr�fen, ob Spezifikationen konsistent sind, also implementiert
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder werden k�nnen
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder - f�r Refinement-Beweise
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder- Algorithmen zur Pr�fung von Erweiterungen, ob diese konservativ,
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder definitional oder monomorph sind
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder - Beschreibung des Algorithmus in Pseudocode
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski - Korrektheitsbeweis, d.h. f�r die Erweiterungen, die der Algorithmus
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski als konservativ erkennt, muss f�r jedes Modell der kleineren
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski Spezifikation eine Modellerweiterung zur gr��eren Spezifikation
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski gefunden werden. Z.B. im Falle von free types kann dies eine
6c82551a9e6a38aa7c774db95ee957379f03df75Christian Maeder Termalgebra-Konstruktion sein.
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski SP1 -- \sigma --> SP2
b303a3717d229b102bca29e58d9e38c2f91fd233Christian Maeder konservativ: jedes SP_1-Modell M1 hat eine Erweiterung zu einem
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski SP2-Modell M2 mit M2|_\sigma=M1.
6c82551a9e6a38aa7c774db95ee957379f03df75Christian Maeder
6c82551a9e6a38aa7c774db95ee957379f03df75Christian Maederport CCC to Haskell
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiFunktionen imageOfMorphism und inhabited
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski mit "cvs add SigFuns.hs" einchecken
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski
566b6a416bde2bc90d3aece2d992127303fb5d75Till MossakowskiNew module FreeTypes.hs:
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski"free datatypes and recursive equations are consistent"
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski
566b6a416bde2bc90d3aece2d992127303fb5d75Till MossakowskicheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiJust True => Yes, is consistent
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiJust False => No, is inconsistent
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiNothing => don't know
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maedercall the symbols in the image of the signature morphism "new"
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maeder
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maeder- each new sort must be a free type,
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maeder i.e. it must occur in a sort generation constraint that is marked as free
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maeder (Sort_gen_ax constrs True)
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maeder such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski if not, output "don't know"
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski and there must be one term of that sort (inhabited)
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski if not, output "no"
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski- group the axioms according to their leading operation/predicate symbol,
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski i.e. the f resp. the p in
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski Implication Application Strong_equation
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski Implication Predication Equivalence
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski if there are axioms not being of this form, output "don't know"
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowskicheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowskicheck' [] = ([([],[])],emptyUniqSet)
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowskicheck' [EqnInfo n ctx ps (MatchResult CanFail _)]
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskicheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski | all_vars ps = (pats, addOneToUniqSet indexs n)
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder where
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder (pats,indexs) = check' rs
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder-- falls ein Konstruktor dabei ist: split_by_constructor
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maedercheck' qs@((EqnInfo n ctx ps result):_)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski | all_vars ps = ([], unitUniqSet n)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski | constructors = split_by_constructor qs
4dcd2d1b64ccc7f705f2ce10d129ef9304ae413bChristian Maeder | only_vars = first_column_only_vars qs
9565b030a2f09eeaac049389e27aa0977212a231Christian Maeder | otherwise = panic "Check.check': Not implemented :-("
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder where
331ed72b03dc966e023fecae5f0116b119082ccdTill Mossakowski -- Note: RecPats will have been simplified to ConPats
0d42a1490aa92c24b19823f745104eefbf29675dChristian Maeder -- at this stage.
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski constructors = or (map is_con qs)
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski only_vars = and (map is_var qs)
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowskisubsort definitions: are conservative if formula is satisfiable
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski (generate proof obligation)
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski************************************************
dedca4980b2d43bc343ffcaf73e0617524f9720cTill MossakowskiHeng (Klaus)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian MaederOWL-DL logic
96cc01853b72b9d0fdc9e3d309a196a2216de119Christian MaederOWL-DL (<)-> CASL-DL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maederemacs mode:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski highlight does not work properly for HasCASL/Set.het or UserManual/Sbcs.casl
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder some operation symbols
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski show hets output immediately
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski C-c C-g for hets -g
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski when hets terminates abnormally (e.g. with a fail), emacs loops
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski C-n jumps to the next error, but the message windows is not always scrolled
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski in such a way that the error is at the top (for long error lists)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich Version for XEamcs?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski should work with parser error messages as well (adapt these?)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichKen (Till)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichlook at command line interface (just call hets)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichimplement simplified rule Theorem-Hide-Shift
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichProofs.TheoremHideShiftSimp
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichtry out examples
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichconservativity calculus
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichweakly amalgamable cocones
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichdevelopment graph calculus
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich(see Sect. IV:4.4 of the CASL Reference Manual)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichlook at Static/DevGraph.hs
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichlook at Proofs/EdgeUtils.hs Proofs/StatusUtils.hs Proofs/Global.hs
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichtest command line interface (just call hets)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichtest development graph GUI:
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich global decomposition
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich menu edit - unnamed nodes - hide/show nodes,
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich node menu: show just subtree / undo
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich interaction with edit - proofs - automatic?
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich use update of uDrawGraph-nodes,edges instead of erasing and adding nodes
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich for attribute changes like color
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichprofiling for "automatic" (look at www.haskell.org/ghc)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichrestrict proofs: only one prove window per node at a given time
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************
aa6f6fa09091e92016598584162b9ba909af48ccTill Mossakowskifurther task 1
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski************************************************
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichfurther task 2
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichUni-Refactoring,
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichmake modules hierarchical, change scoped type variables for ghc-6.5
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich(and older ghcs), replace deprecated code (i.e. FiniteMap, hslibs),
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiuse HaXml as a cabalized library, provide uni as (one?) cabal
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskipackage(s), uni used to work under windows as well, watch the
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskii.e. FilePath, Process discussions (libraries@haskell.org)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskipossibly switch to a subversion repository, talk to Achim
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski(amahnke@tzi.de)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskifurther task 3
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskilook fgl/Data/Graph/Inductive/Graph.hs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskilook at Static/DevGraph.hs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskichange management
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski reload button im Edit-Men� hinzuf�gen (GUI/ConvertAbstractToDevgraph.hs)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski reload macht folgendes:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski lade CASL-Datei neu ==> neuer Entwicklungsgraph
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski vergleiche alten+neuen Entwicklungsgraph, konstruiere eine
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Abbildung (Common/Lib/Map.hs) von alt nach neu
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (jeweils eine Abblidung f�r Knoten und eine f�r Kanten)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Kriterien f�r Finden der Knotenabbildung:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski - Namen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski - DGOrigin
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski - Signatur
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskieinfaches Merge von lokalen Beweisen eines abgespeichteren DG
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski in aktuellen DG
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
42e6f81f0794a7b6bc8e29e97c55668abe96da59Till Mossakowskifurther task 4
42e6f81f0794a7b6bc8e29e97c55668abe96da59Till Mossakowski************************************************
42e6f81f0794a7b6bc8e29e97c55668abe96da59Till Mossakowski
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowskigraph of Haskell module dependencies
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowski using .import files
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowski
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowski************************************************
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowskifurther task 5
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowski************************************************
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowski
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowskiport hets to windows. -- costs too much energy at this stage! Till
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowski
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till MossakowskiIf hets should become successful then requests for support under
ec75b50a89aea0d96fd19ce864225267d0625f25Till Mossakowskiwindows will surely follow.
ec75b50a89aea0d96fd19ce864225267d0625f25Till Mossakowski
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiGhc, uni and uDrawGraph should work under windows. Only Isabelle does
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskinot exist for windows, but SPASS does. Probably only a few path
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskicomputations need to be adapted (made modular) within hets. Also
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskiposition computations (of Parsec) should be checked under windows.
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski************************************************
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskifurther task 6
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski************************************************
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskirefactor pretty printing
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskieine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskiund andere Formate besser zu unterst�tzen und einheitlichen PP code
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski(independent from GlobalAnnos) f�r die (Het-)CASL (and HasCASL!)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiDatentypen (particularly for HasCASL data types) zu bekommen.
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiLaTeX: see listings.sty for LaTeX generation (cf. CoSiT paper)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski************************************************
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskiremaining stuff
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski************************************************
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskiset up a ticket and tracking systems (for bugs and features) instead
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskiof this messy todo list
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski--> sourceforge???
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskirefactoring of dgraphs: add unique tags + hashes (but no table)
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski how to compare complex datastructures:
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski tag x1==tag x2 || (hash x1==hash x2 && x1==x2)
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskidisplay library graph
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskiunify GUI/AbstractGraphView.hs and Taxonomy/AbstractGraphView.hs
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskiand uni/appl/ontologytool/AbstractGraphView.hs
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski(make it really abstract), possibly contact amahnke@tzi.de regarding
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiTaxonomy, possibly use uni/appl/ontologytool instead of Taxonomy!
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskiset up default simplifier
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskiset up default tactics using axioms
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski (see DOLCE sample files)
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowskiimprove efficiency (e.g. of UserManual/Sbcs.casl), using profiling
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski************************************************
f157913a0128ce772d0acd5038f61a7a619fd707Till MossakowskiDaniel
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski************************************************
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowskigenerate infrastructure for circular coinduction
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till MossakowskiCCS example: commutativity of || by coinduction
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski
21d72ad1e64e2fa6d831f9def45d6dc21f6e0bd8Till Mossakowski************************************************
21d72ad1e64e2fa6d831f9def45d6dc21f6e0bd8Till MossakowskiChristian
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski************************************************
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski
cb1c5be39138fb8f037dbefc121fe41adc06845dTill MossakowskiIsabelle coding
601f11cf0b4164a6a718038a736ae3d579f3a27cTill Mossakowski- improve display syntax in HasCASL-Isabelle coding
601f11cf0b4164a6a718038a736ae3d579f3a27cTill Mossakowski- identifiers in mixfix templates must be excluded as ordinary
7ed2a775680fb1a29e6907d372124906b7746420Till Mossakowskiidentifiers (i.e. as quantified variables)
7ed2a775680fb1a29e6907d372124906b7746420Till Mossakowski
7ed2a775680fb1a29e6907d372124906b7746420Till Mossakowski
8980a8c8137a3a4c69bf9fdb3eca5b4b7f6e69c9Till Mossakowskimore abstract datatypes?
8980a8c8137a3a4c69bf9fdb3eca5b4b7f6e69c9Till Mossakowski
aa6f6fa09091e92016598584162b9ba909af48ccTill Mossakowskicollect the patches for programatica (or create a package)
85ab61b931e22a72a53628b8aa5d059eeaedf1bdTill Mossakowski- conv (SN i p) = PN i (S p)
85ab61b931e22a72a53628b8aa5d059eeaedf1bdTill Mossakowski+ conv (SN i p) = PN i (Sn (show i) p)
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskiin programatica/tools/base/parse2/NumberNames.hs
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskifixes translation error of Pair
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskisimplification of HasCASL sentences (omit types)
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiLogic COL is a ruin
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskilogic coding from the comand line with printing of results
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiHaskell modules: hiding, renaming
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski- group the axioms according to their leading operation/predicate symbol,
331ed72b03dc966e023fecae5f0116b119082ccdTill Mossakowski i.e. the f resp. the p in
331ed72b03dc966e023fecae5f0116b119082ccdTill Mossakowski forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
331ed72b03dc966e023fecae5f0116b119082ccdTill Mossakowski forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
b2768faecd6610af357407a8ddfe1412a18f8ebcChristian Maeder if there are axioms not being of this form, output error
60082d649e5bbb1c54f73f8921c3c390170e6c46Till Mossakowski
950ecce40ed5a97adf4460be07b47e3a0d0b1e56Till Mossakowski
60082d649e5bbb1c54f73f8921c3c390170e6c46Till MossakowskiStatic analysis for HasCASL
617a89d712d108f8d4c2bfe888a7e59566d17c0eTill Mossakowski pattern analysis for program equations
617a89d712d108f8d4c2bfe888a7e59566d17c0eTill Mossakowski implemented only atomic subtyping
3e2c4de10a0eb284938b5d5307d1c1fc2f799456Till Mossakowski
3e2c4de10a0eb284938b5d5307d1c1fc2f799456Till MossakowskiWeak amalgamation analysis?
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiInstantiate Transformation Application system for HasCASL?
dedca4980b2d43bc343ffcaf73e0617524f9720cTill MossakowskiAutomatic generation of Haskell (for a HasCASL subset)
4be2c76af9603b48b147f1f369f713e78544974eTill MossakowskiProofs in HasCASL
4be2c76af9603b48b147f1f369f713e78544974eTill MossakowskiCase study
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
331ed72b03dc966e023fecae5f0116b119082ccdTill Mossakowski
e539b8cb4a47f987bc57c90ee964219ac53841ffTill MossakowskiCoding HasCASL -> Isabelle with definedness axioms
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski only strict functions are defined
60082d649e5bbb1c54f73f8921c3c390170e6c46Till Mossakowski
60082d649e5bbb1c54f73f8921c3c390170e6c46Till MossakowskiIsabelle interface
60082d649e5bbb1c54f73f8921c3c390170e6c46Till Mossakowski One emacs with spec and proof buffer
60082d649e5bbb1c54f73f8921c3c390170e6c46Till Mossakowski Reload button should rebuild buffers while keeping as much as possible
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski keep structuring of Hets theories
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski************************************************
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiRainer (Klaus)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski************************************************
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski
e539b8cb4a47f987bc57c90ee964219ac53841ffTill MossakowskiSPASS encoding improvements in SPASS.Conversions/Comorphisms.CASL2SPASS
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski - if there is only one sort in the signature eliminate it
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski special case: (freely) generated sorts are not eliminated
04d17d4f8862860f968f6b72b902163aacda6343Till Mossakowski new flag in SPASS sign: singleSorted
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski Sentences are modified in CASL2SPASS
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski all variable declarations have to consider the flag
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski (quantified formulas) variable lists without types
2d76902bf3b380a32268ccc0d2cd9e376988a060Till Mossakowski Formula/Term specific
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski - F:Membership ==> true
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski - T:Cast is omitted
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski - T:Sorted_term is omitted
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski typings in the signature have to be removed in SPASS.Conversions
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski empty declarations list
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiSPASS encoding improvements in CASL2SPASS
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski - if there are predicates defined upon equality substitute them with equality
b2768faecd6610af357407a8ddfe1412a18f8ebcChristian Maeder and remove them from the signature
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski find definitions (Equivalences) where one side is a binary predicate
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski and the other side is a builtin equality application (Strong_equation)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski return the full qualified (with type) predicate(s)
331ed72b03dc966e023fecae5f0116b119082ccdTill Mossakowski this is done before the translation of the signature/sentences happens
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski remove eqPrediate symbols from signature
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski substitute eqPredications with Strong_equation in the Formulas
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski see CASL.Utils.codeOutConditionalF
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiKlaus
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
2ee1615e999c5e0c49508ed4fcced7344b050042Till Mossakowskifor ProofManagement-GUI
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski mark imported theorems for selection
f69658e57cba7ecb37c0d84181f4c563215c2534Till Mossakowski provide structured (based on spec-names) selection/deselection facility
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski of axioms and theorems
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskitrace if liniarity of sentences along development is given
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskifor consistency checking with Isabelle, look at the following SAT-Solvers:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMChaff, ZChaff, Berkmin
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiConsistency checker interface
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski via global interface, accessible from global and node menus
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski use falseSentence from Logic.Logic (property: holds in no model)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski proved -> inconsistent
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski disproved -> consistent (assuming completeness)
31c49f2fa23d4ac089f35145d80a224deb6ea7e4Till Mossakowski batch mode for automatic provers such as SPASS
31c49f2fa23d4ac089f35145d80a224deb6ea7e4Till Mossakowski (use automatic flag for provers)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskibatch interface for Isabelle
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski each goal is proved separatedly, with a time limit enforced
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski by killing the process
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski the tactic is
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski "using Ax1 ... Axn by auto"
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski where Ax1 ... Axn is the list of all axioms.
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski "auto" could be replaced with "best", "blast" etc. (user selection)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIgnore axiom selection for interactive provers
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiTranslation between Achim's ontology data structure and CASL (in Hets)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskivisualization of "taxonomy" of CASL signatures
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (subsorts = inheritance, unary preds = concepts, binary preds = relations)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski last two ... partially done
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
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 Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiJoost Visser wg. ATerms in Haskell => neues Repository
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMarkus, Lutz
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiBeweise in Isabelle
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiCASL consistency checker
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski (Vorbild: Larch-Handbuch)
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
cc7492cd222f08d17c994912bcb0c60083ae2bc9Till MossakowskiParser and static analysis for CSP-CASL
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiChristoph
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski************************************************
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCASL consistency checker
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIntegration with generic prover interface?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiTill
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskienhance Web interface with SPASS (%implied, consistency)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskitranslation of proofs along comorphisms (it this necessary at all???)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski use inverse morphism?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski leads to translation of G_theory along comorphism that also
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski keeps proof status info
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski this may be used in GUI prover interfaces for recovering old proof attempts
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski and offering them as default
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiproveCMDLinteractive (PGIP)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiModel expansion flag for comorphisms
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUmlaute in daVinci anzeigen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiFragen an Michael:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiwerden Links in der richtigen Reihenfolge geschrieben (S. 183 OMDoc)?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski was ist dort eigentlich das Problem?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCodierung von Subsorten?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskipaper with Paolo
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski semantic adequecy of HOL translation
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRegulate concurrent proving
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski.dg files: store only current library; import .dg files for other libraries
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMarkus' Bsp:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIsabelle: use meta-quantifiers
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskilocal subsumption ?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskibetter syntax (Tina)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskicheck for proved theorems
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAbstractGraphView: switch to Result monad
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiunite or rename consCheck and cons_checkers
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiBinInt.casl: revealing in Int1 does not work correctly
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskifrom Stefan W�lfl:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskicomputeTheory does not work across library imports
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskilocal theorems
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiall nodes named
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskihierarchical Isabelle theories
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskidaVinci printing is not adequate
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskihiding of internal nodes does not work
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCSPs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski----
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiFOL without quantifiers and with uniform disjunctions
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (i.e. x R1 y \/ x R2 y)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (with and without =)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskialgorithmic path consistency over a relation algebra
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski plug in reasoner for this
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski develop correctness results (algorithmic path consistency=path consistency)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski within CASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCASL sublogics:
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski---------------
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiFOL without quantifiers (with and without =)
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskiguarded fragment
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiProp
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski[from DOLCE cooperation:
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskiquit wish!
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskiontology mediation via pushouts/pullbacks/pulations
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiRobinson consistency with shared theory constructed via pre-image?
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskishow theorem links between same instances of different parameterized
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski specs (where one is an extension of the other one)
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskilink menu for %implies, $def, %cons, even without open proof obligation
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskifor a proved theorem, show minimal part of DG needed for proof
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskicons, def, mono for nodes
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiIsabelle interface: each qed should write proof info into file
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowskiglobally display nodes containing symbols mapped "twice" (i.e. via
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski different signature morphisms)
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski and add a menu for each node allowing for tracking the different
uses of the symbols/concepts
topsort coding: partial functions as relations?
]
theorem link menu for proof obligations
UserManual/Chapter7.casl: local thm link starting from Monoid leads to type error
in Isabelle. Reason: Inlineaxioms does not translate ga_totality axioms
correctly.
Buffer.het, sublogic of node Buffer:
Fail: illegal node type in sublogic computation
J�rgen Zimmer, Saarbr�cken+Edinburgh, Beweiserkennung f�r versch. Logiken im MathWeb
for CSP-CASL example: with logic
heterogeneous static ana
theorem links between nodes in different libraries
basicProofs: use info about used axioms
ensure that axiom/thm names are unique
Overload / inlineAxioms: injections
remove "prove" menu in abstracted dg
better sublogic analysis in codings
thy files in subdir
adjust path for thy files, such that hets can also be started from subdirs
Restrict Sonjas simplifications to HasCASL
add suitable axioms to simplifier and CR
computeTheory: remove double axioms
add suitable axioms to simplifier and classical reasoner
better display of internal nodes (use tooltip?)
update Hets, CASL, daVinci on web page
CASL2PCFOL: x_i -> t_i, t=[inj(x_i)] (and what not!)
packing of binaries: add hets-update, refer to TclTk
CCC interface
test for sublogic before applying comorphism
Missing points for heterogeneous WADT 04 example:
- coding to Isabelle: translate sort gen constraints
- Improve adapation to Isabelle's lexis
Isabelle: (ask Christoph)
remove datatypes from sort list
prove local thm link (=> green)
"prove" menu with choice windows
incorporate sublogics
sublogic translation table
better interaction between Isabelle instance (for one node)
+ selection of single goals that are proved
=> use PGIP interface (Christoph, David)
correct show theory
Keep proofs and lemmas in .thy files (kind of merge)
CASL-like syntax
CASL annotation for lemmas that should be used in proof
inherit CASL's mixfix syntax
Signatures versus theories: where to store additional infos?
comp(id,x)=x for comorphism names
Generalise CASL2Modal
Mixfix analysis + typecheck for modality axiomatizations
Modal logics: modal logic, temporal logic, mu calculus
+ translations (e.g. modal to FOL)
CASL->Haskell with free DTs (mark sortgens) + recursion
- List[Dec] wird List[Pos]
- node numbers do not match
- thm links with external target should be provable as well
Remove warnings
Different types of logic translations
Improve Static analysis of structured specs
Development graph calculus, Strategies for DG rules
use graph grammars to model rules? transformation units?
Management of change
Integrate provers
Otter model checker
FOL-prover by Uli Furhbach
modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
Isabelle codings: www.inf.ethz.ch/~vigano
Renate Schmidt, Manchester: uses FOL prover for description logic
(as efficient as DL-specific tools!)
Look at PROSPER toolkit
consistency: see IJCAR-workshop on non-provability in Cork
IJCAR workshop about logical frameworks and meta-languages
Integrate CCC
Encodings
Errors:
Klaus' wayfinding example
ask Detlef: critical pairs, Fossacs paper by Francesco
UniForM workbench:
first steps towards CASL instance, using ATerms and re-using MMISS instance
variants for specs (needed for DOLCE: CASL variant, DL variant, ...)
Integration of MAYA and Isabelle/HOL (global HOL-Coding of
Grothendieck logic)
+ for TAS: reflection of HOL in HOL, to be composed with encodings
(i.e. signatures, axioms, signature morphisms in HOL,
re-use ML signatures) (Einar)
Display Specs as daVinci subgraphs
User interface
--------------
Logic graph window
Input text window
Development graph window
Prover windows
************************************************
FOR STUDENTS
************************************************
Hets 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)
Packaging of installation
GUI (vgl. VSE)
with Eclipse, WXHaskell or GTk?
how to integrate with event system of UniForM workbench?
integrate graphviz (or use Java interface for racer? or Isabelle browser? or...?)
this interacts with GUI!
Data.Serizable (only when ghc supports it) better: rely on pointer equality
XML interface
increase performance
integrate QuickCheck: come to lecture!
++++++++++++++++++++++++++++++++++++++++++++++++
Remaining things
++++++++++++++++++++++++++++++++++++++++++++++++
Mark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
Coq, PTT in Maude
Proofs with basic datatypes
Verbesserung der Fehlermeldungen
Improve encoding: CATS/basic_encode.sml (3 days)
More HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
Renamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)
Example of Agnes und Frank: proofs in HOL-CASL (2 days)
Term input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
Examples for cond rewriting -> Christophe
Doku: VSE-Prover, VSE-Method VSE-demo in Bremen?
Adapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
Eigene IsaWin-Instanz mit CASL-RS statt HOL-RS
HOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)
HOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)
HOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)
Encoding of structured free (3 days)
Encoding of structured cofree (2 weeks)
Eingabesyntax als Mix zwischen CASL und HOL (3 days)
Adapt Isabelle unions to CASL unions (1 week)
IsaWin git/src/isa_ext/casl_thy.sml (1 week)
Generate Proof obligations (1 week)
Add renaming to Isabelle kernel (2 months)
Basic datatypes CASL-lib/Basic/basic.casl
Repository mit korrekten und fehlerhaften Specs
HetCATS User manual, Doku fuer Environments (2 weeks)
Conversion ASF/SDF-Parser -> abstract syntax (in Haskell)
Comparsion of parsers (ML-yacc parser, SDF-Parser)
Conversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren
PVS anbinden (Kooperation mit Cachan?)
Portations: Intel-Solaris, Mac OS-10 (2 weeks)
(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm
Views on CASL specs: CATS/viewer.sml (2 weeks)
Uebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
Module graph CATS/module_graph.sml (1 week) -> Maya?
ATerms via XML: CATS/aterms.sml (2 weeks)
Neues Tool-Schaubild auf Web-Seiten ver�ffentlichen
Library management: CATS/lib_ana.sml (2 weeks)
Version management/Uniform Workbench: CATS/lib_ana.sml (2 months)
{- This does not work due to needed ordering:
instance Functor Set where
fmap = mapSet
instance Monad Set where
return = unitSet
m >>= k = unionManySets (setToList (fmap k m))
-}
Aufbau von comptable
--------------------
[("normal","normal","normal"),
("normal","inclusion","normal"),
("inclusion","normal","normal"),
("inclusion","inclusion","inclusion")]
Aufbau von ginfo
--------------------
Mit initgraphs erzeugen
Aufbau des Graphen selbst
------------------------
addnode
addlink