todo revision 2d6b942b2d10709143b699783f38957d8856e67f
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPlan and priority list for CoFI tool activities
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski************************************************
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski************************************************
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till MossakowskiHaskell parser f�r XHaskell erweitern
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till MossakowskiDiplom: Encoding for HasCASL in Isabelle/HOL(CF)
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till MossakowskiHaskell modules: hiding, renaming
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski************************************************
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski************************************************
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowskidevelopment graph calculus
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski- Stack overflow for "show just subtree"
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski- view-test7.casl should be provable with globDecomp + locDecopm
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski- fail when doing first globDecomp, then local decomp in RelationsAndOrders
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski- correct MAYA: glob decomp: some links are not found (Jorina)
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski************************************************
db373255bd95ce4de47dde876c3a3bfc49c22a97Till Mossakowski************************************************
db373255bd95ce4de47dde876c3a3bfc49c22a97Till Mossakowskitype check for CASL
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski*** Error encode.casl:8.30, No correct typing for
2b60e1b81de56782be899de982c0908696f3530dTill Mossakowski************************************************
2b60e1b81de56782be899de982c0908696f3530dTill Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiport CCC to Haskell
38f30f746aa42d4fc659a15e183801f2f74596d0Till MossakowskiFunktionen imageOfMorphism und inhabited
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till 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
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski Implication Application Strong_equation
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
2d6b942b2d10709143b699783f38957d8856e67fTill Mossakowski Implication Predication Equivalence
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till Mossakowski if there are axioms not being of this form, output "don't know"
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski************************************************
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiZicheng (Till)
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski************************************************
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiTranslation from CASL with subsorts to CASL without subsorts
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskisee CATS/basic_encode.sml, encode SubCFOL into CFOL
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskiencode subsorting by injection functions
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski1. translation of signatures (see HetCATS/CASL/Sign.hs)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski2. genertion of axioms (injectivity, overloading ...)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskidetails: see paper in Theoretical Computer Science, p. 407
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski************************************************
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski************************************************
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiDarstellung des Logik-Graphen
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskidazu importieren:
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski-- f�r Graph-Darstellung
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskiimport DaVinciGraph
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskiimport GraphDisp
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskiimport GraphConfigure
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski-- f�r Erzeugen von Fenstern
a1bb9f8f9143aa2d84dfab69ed988d94f7e3b196Till Mossakowskiimport TextDisplay
a1bb9f8f9143aa2d84dfab69ed988d94f7e3b196Till Mossakowskiimport Configuration
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiimport qualified HTk
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiplus unten genannte Module
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAufgabe: den Logik-Graph aus folgendem Modul:
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich logicGraph aus Comorphisms/LogicGraph.hs, Typ in Logic/Grothendieck.hs
e1f2ef9a7f4d41a42927b2e352cbb558791a4007Klaus Luettichaufbereiten f�r Anzeige, Vorbild ist in uni/graphs/test/GraphDispTest.hs
f157913a0128ce772d0acd5038f61a7a619fd707Till MossakowskiAufbau von nodeTypeParams
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski-------------------------
f157913a0128ce772d0acd5038f61a7a619fd707Till MossakowskiKnoten (bzw. Kanten) habe Werte, in diesem Fall: AnyLogic (bzw. AnyComorphism)
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowskinur 1 Knotentyp, rund, gr�n
87268d03b727bc9091716644fcf4048379accf02Till MossakowskiMen�funktionen AnyLogic -> IO ()
87268d03b727bc9091716644fcf4048379accf02Till MossakowskiValueTitle AnyLogic -> String (= language_name aus Logic/Logic.hs)
87268d03b727bc9091716644fcf4048379accf02Till Mossakowski$$$ ist Funktion zum Zusammenf�gen von Knotentyp-Parametern
aa6f6fa09091e92016598584162b9ba909af48ccTill Mossakowskiunter Men�eintrag "Info" anzeigen: Werte aus Logic/Logic.hs
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskierstmal AnyLogic-Wert auspacken, z.B. mit
e1f2ef9a7f4d41a42927b2e352cbb558791a4007Klaus LuettichLogik-Namen ausgbene (mit language_name lid)
b021b399b59fb7009308ed7a3eda30182dea7976Klaus LuettichTest auf Just _, dann String ausgeben
b021b399b59fb7009308ed7a3eda30182dea7976Klaus Luettichparse_basic_spec lid "Parser for basic specifications"
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskiparse_symb_items lid "Parser for symbol lists"
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskiparse_symb_map_items lid "Parser for symbol maps"
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskiparse_sentence lid "Parser for sentences"
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskibasic_analysis lid "Analysis of basic specifications"
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskidata_logic lid "is a process logic"
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maedermap (sublogic_names lid) (all_sublogics lid)
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maeder -- sp�ter besser als eigener Men�punkt ==> eigener Graph
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maedermap prover_name (provers lid) -- aus Logic/Provers.hs
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maedermap cons_checker_name (cons_checkers lid)
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian MaederAnzeigen dieser Ausgabe mit:
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maeder createTextDisplay title str [size(100,50)]
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maederstr ist der anzuzeigende Inhalt
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiAufbau von arcTypeParams
e1f2ef9a7f4d41a42927b2e352cbb558791a4007Klaus Luettich-------------------------
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till Mossakowski- einen "normal" f�r "normale" Comorphismen, schwarz
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till Mossakowski- einen "inclusion" f�r Inclusions, blau
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till MossakowskiKantenmen�: Anzeige von sourceSublogic und targetSublogic (siehe Logic/Comorphisms.hs)
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till Mossakowskimittels language_name
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till MossakowskiAufbau des Graphen selbst
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski------------------------
420440d8d1a274241aae513044f0f9a0bc691985Christian MaederGraphDisp.newGraph daVinciSort -- aus uni/graphs/GraphDisp.hs
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder -- mit leerem globalen Men�
420440d8d1a274241aae513044f0f9a0bc691985Christian MaederAnzeige des Graphen
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder-------------------
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder-------------------------------------------------------------------
420440d8d1a274241aae513044f0f9a0bc691985Christian MaederLaTeX pretty printer
420440d8d1a274241aae513044f0f9a0bc691985Christian Maedervon Christian:
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskia) analysierte Formeln und Terme optimal/k�rzer ausgeben:
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskishorten :: Sign -> {TERM, FORMULA} -> {TERM, FORMULA}
6c82551a9e6a38aa7c774db95ee957379f03df75Christian MaederIn Abh�ngigkeit von Sign werden z.B. nicht-�berladene Funktionen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiunqualifiziert ausgeben bzw. zwecks Eindeutigkeit wird (minimal) nur
b303a3717d229b102bca29e58d9e38c2f91fd233Christian Maedermit dem Ergebnistyp qualifiziert.
6c82551a9e6a38aa7c774db95ee957379f03df75Christian Maeder((a: Nat) + (b: Nat)): Nat
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowskib) eine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskiund andere Formate besser zu unterst�tzen und einheitlichen PP code
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskif�r die CASL Datentypen zu bekommen.
566b6a416bde2bc90d3aece2d992127303fb5d75Till MossakowskiHasCASL hat auch noch keine Mixfix- und Latex Ausgabe.
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski************************************************
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski************************************************
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski- group the axioms according to their leading operation/predicate symbol,
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski i.e. the f resp. the p in
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maeder forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maeder forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maeder if there are axioms not being of this form, output error
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian MaederMissing points for heterogeneous WADT 04 example:
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski- improve display of HasCASL sigs + mors
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiStatic analysis for HasCASL
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski checking class constraints of terms
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski pattern analysis for program equations
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski - for simple types (currently type synonyms)
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski symbol representation
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski symbol map analysis (hiding sub/supertypes)
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiWeak amalgamation analysis?
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiInstantiate Transformation Application system for HasCASL?
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiAutomatic generation of Haskell (for a HasCASL subset)
f3a84cc409ed345569be6673d05072dcb4291ebeTill MossakowskiProofs in HasCASL
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski************************************************
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski************************************************
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowskivisualization of "taxonomy" of CASL signatures
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (subsorts = inheritance, unary preds = concepts, binary preds = relations)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRecognize guarded fragment of CASL:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski G ::= forall x . At(x) => G where At is a conjunction of atoms
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski | exists x . At(x) /\ G
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian MaederJoost Visser wg. ATerms in Haskell => neues Repository
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder************************************************
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder************************************************
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiBeweise in Isabelle
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiCASL consistency checker
4dcd2d1b64ccc7f705f2ce10d129ef9304ae413bChristian MaederWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
9565b030a2f09eeaac049389e27aa0977212a231Christian Maeder (Vorbild: Larch-Handbuch)
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian MaederSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
331ed72b03dc966e023fecae5f0116b119082ccdTill MossakowskiParser and static analysis for CSP-CASL
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski************************************************
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski************************************************
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill MossakowskiCASL consistency checker
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill MossakowskiIsaWin: support CASL-libraries
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian MaederStatic analysis of architectural specs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMissing points for heterogeneous WADT 04 example:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- coding to Isabelle: translate sort gen constraints
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- correct display of CASL sublogis
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich- extended globDecomp rule: existing local Thm links
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (e.g. generated by %implied) should lead to fewer new local
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski links ("local composition" rule)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich- Improve adapation to Isabelle's lexis
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichIsabelle: (ask Christoph)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich free datatypes
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich prove local thm link (=> green)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich better interaction between Isabelle instance (for one node)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich + selection of single goals that are proved
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich => use PGIP interface (Christoph, David)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich correct show theory
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich Keep proofs and lemmas in .thy files (kind of merge)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich CASL-like syntax
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich CASL annotation for lemmas that should be used in proof
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich inherit CASL's mixfix syntax
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichSignatures versus theories: where to store additional infos?
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichcomp(id,x)=x for comorphism names
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichGeneralie CASL2Modal
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichMixfix analysis + typecheck for modality axiomatizations
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichModal logics: modal logic, temporal logic, mu calculus
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich+ translations (e.g. modal to FOL)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichComorphisms: also map of theories; with default definition
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichCASL->Haskell with free DTs (mark sortgens) + recursion
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichCoding of subsorts as unary predicates (for ontologies)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichTranslation between Achim's ontology data structure and CASL (in Hets)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich- List[Dec] wird List[Pos]
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich- George wg. Schlie�en von Fenstern
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich- node numbers do not match
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich- thm links with external target should be provable as well
aa6f6fa09091e92016598584162b9ba909af48ccTill MossakowskiRemove warnings
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiDifferent types of logic translations
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiImprove Static analysis of structured specs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDevelopment graph calculus, Strategies for DG rules
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichManagement of change
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichIntegrate provers
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich Otter model checker
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich FOL-prover by Uli Furhbach
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich 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
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich consistency: see IJCAR-workshop on non-provability in Cork
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski IJCAR workshop about logical frameworks and meta-languages
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiKlaus' wayfinding example
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUniForM workbench:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskifirst steps towards CASL instance, using ATerms and re-using MMISS instance
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskivariants for specs (needed for DOLCE: CASL variant, DL variant, ...)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIntegration of MAYA and Isabelle/HOL (global HOL-Coding of
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Grothendieck logic)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski + for TAS: reflection of HOL in HOL, to be composed with encodings
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (i.e. signatures, axioms, signature morphisms in HOL,
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski re-use ML signatures) (Einar)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDisplay Specs as daVinci subgraphs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUser interface
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski--------------
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiLogic graph window
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiInput text window
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDevelopment graph window
42e6f81f0794a7b6bc8e29e97c55668abe96da59Till MossakowskiProver windows
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowski************************************************
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowski************************************************
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till MossakowskiHets Web interface (cf. CATS/web_interface2.sml)
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till MossakowskiPackaging of installation
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowskiintegrate QuickCheck
ec75b50a89aea0d96fd19ce864225267d0625f25Till MossakowskiGUI (vgl. VSE)
ec75b50a89aea0d96fd19ce864225267d0625f25Till Mossakowskiincrease performance
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski++++++++++++++++++++++++++++++++++++++++++++++++
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiRemaining things
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski++++++++++++++++++++++++++++++++++++++++++++++++
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiMark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski Coq, PTT in Maude
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiProof general interface (1 day)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiTest Maya with basic datatypes
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiVerbesserung der Fehlermeldungen
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiImprove encoding: CATS/basic_encode.sml (3 days)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiMore HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiRenamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiExample of Agnes und Frank: proofs in HOL-CASL (2 days)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiTerm input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiExamples for cond rewriting -> Christophe
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiDoku: VSE-Prover, VSE-Method VSE-demo in Bremen?
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiAdapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiEigene IsaWin-Instanz mit CASL-RS statt HOL-RS
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiHOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiHOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiHOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiEncoding of structured free (3 days)
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiEncoding of structured cofree (2 weeks)
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiEingabesyntax als Mix zwischen CASL und HOL (3 days)
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiAdapt Isabelle unions to CASL unions (1 week)
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiIsaWin git/src/isa_ext/casl_thy.sml (1 week)
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiGenerate Proof obligations (1 week)
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiAdd renaming to Isabelle kernel (2 months)
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiRepository mit korrekten und fehlerhaften Specs
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiHetCATS User manual, Doku fuer Environments (2 weeks)
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiConversion ASF/SDF-Parser -> abstract syntax (in Haskell)
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiComparsion of parsers (ML-yacc parser, SDF-Parser)
f157913a0128ce772d0acd5038f61a7a619fd707Till MossakowskiConversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren
f157913a0128ce772d0acd5038f61a7a619fd707Till MossakowskiPVS anbinden (Kooperation mit Cachan?)
f157913a0128ce772d0acd5038f61a7a619fd707Till MossakowskiPortations: Intel-Solaris, Mac OS-10 (2 weeks)
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till MossakowskiViews on CASL specs: CATS/viewer.sml (2 weeks)
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till MossakowskiUebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till MossakowskiModule graph CATS/module_graph.sml (1 week) -> Maya?
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till MossakowskiATerms via XML: CATS/aterms.sml (2 weeks)
21d72ad1e64e2fa6d831f9def45d6dc21f6e0bd8Till MossakowskiNeues Tool-Schaubild auf Web-Seiten ver�ffentlichen
cb1c5be39138fb8f037dbefc121fe41adc06845dTill MossakowskiLibrary management: CATS/lib_ana.sml (2 weeks)
cb1c5be39138fb8f037dbefc121fe41adc06845dTill MossakowskiVersion management/Uniform Workbench: CATS/lib_ana.sml (2 months)
7ed2a775680fb1a29e6907d372124906b7746420Till Mossakowski{- This does not work due to needed ordering:
8980a8c8137a3a4c69bf9fdb3eca5b4b7f6e69c9Till Mossakowskiinstance Functor Set where
8980a8c8137a3a4c69bf9fdb3eca5b4b7f6e69c9Till Mossakowski fmap = mapSet
aa6f6fa09091e92016598584162b9ba909af48ccTill Mossakowskiinstance Monad Set where
85ab61b931e22a72a53628b8aa5d059eeaedf1bdTill Mossakowski return = unitSet
85ab61b931e22a72a53628b8aa5d059eeaedf1bdTill Mossakowski m >>= k = unionManySets (setToList (fmap k m))
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiAufbau von comptable
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski--------------------
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski[("normal","normal","normal"),
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski ("normal","inclusion","normal"),
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski ("inclusion","normal","normal"),
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski ("inclusion","inclusion","inclusion")]
331ed72b03dc966e023fecae5f0116b119082ccdTill MossakowskiAufbau von ginfo
331ed72b03dc966e023fecae5f0116b119082ccdTill Mossakowski--------------------
331ed72b03dc966e023fecae5f0116b119082ccdTill MossakowskiMit initgraphs erzeugen
60082d649e5bbb1c54f73f8921c3c390170e6c46Till MossakowskiAufbau des Graphen selbst
950ecce40ed5a97adf4460be07b47e3a0d0b1e56Till Mossakowski------------------------