todo revision 8b3384c16fc380424b24dc5ddc9bc1cecc726efb
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
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
Plan and priority list for CoFI tool activities
************************************************
Immanuel
************************************************
Suchfunktion f�r einen Knoten im DG:
welche anderen Knoten sind hier mit Theoriemorphismus abbildbar?
erstmal auf eine Logik (z.B. CASL) beschr�nken
- Funktion f�r Morphismus-Suche zwischen Theorien
- evtl. angucken: CASL.SymbolMapAnalysis, inducedFromToMorphism Map.empty
RawSymbolMap als "Suche-Guide" wird erestzt durch Axiome/Theoreme
- Einbindung ins GUI (GUI.ConvertAbstractToDevGraph)
BasicProof in Proofs.Proofs: sind Datenstrukturen f�r informelle Beweise OK?
Konfidenzgrade von Beweisen?
von Till/HiWi zu erledigen:
Repr�sentation �ndern:
Beweisobjekte an DGs, nicht an Regeln -- done
F�r Theoreme in Theorien an Beweisobjekte -- done
BasicProof mit Liste von Beweisobjekten -- �berfl�ssig
Definitionen auszeichnen -- done
F�r alles siehe G_theory, ThSens und SenStatus.
Isabelles Beweisobjekte einbinden
************************************************
Razvan (Till)
************************************************
Integration with PGIP
Hets needs to be equipped with a command-line interface that reads in
specification libraries and proof commands
Proof commands are special annotations in the libraries
All menu commands of the development graph interface (GUI/...) should become (proof) commands
when stepping through the specs, dg calculus generates proof obligations
(for the current dg node only),
which then can be discharged by Isabelle, SPASS etc.
That is, the proof commands always occur at the position in the text
that generates the dg node?!? or should they occur after each specification?
needs incremental parsing and static analysis for Hets libraries
easy: parse and analyse one specification at a time, and then process it with proof commands
more challenging: incrementally parse and analyse also individual specifications
************************************************
Anton (Till)
************************************************
Modal-CASL <-> CASL-DL
see Chapter 4 of "The Description Logic Handbook"
and ask Klaus for a print out of it
improve Modal-CASL
possibly also modal logic in CoCASL
**************** task A ************************
Proofs with Isabelle and SPASS
CASL basic datatypes
HasCASL examples
- improve simplifier for partiality in Isabelle coding
program interaction between solver, subgoaler and simplifier in such a way
that proofs of definedness conditions are postponed
************************************************
Florian (Till)
************************************************
Modelchecker f�r algebraische Eigenschaften
neue Hets-Option in Driver/WriteFn.hs implementieren
hets -n NonAssocRelationAlgebra
--modelSparQ=datei.lisp Calculi/Algebra/RelationAlgebra.casl
(oder -m datei.lisp)
siehe auch CASL.CompositionTable.ComputeTable
modelCheck :: SIMPLE_ID -> (Sign f e, [Named (FORMULA f)])
-> Result Bool
Warnung mit Gegenbspen ausgeben, wenn eine Eigenschaft nicht gilt
(abbrechen nach 10 Gegenbspen)
Warnungen erzeugen mit Funktion warning aus Common.Result
Range aus den CASL-FORMULAs extrahieren
Result ist eine Monade, ggf. mit do-Notation arbeiten
Pr�fung der G�ltigkeit von CASL-Formel in einer Table, rekursiv:
Allquantoren --> all, Existenzquantor --> any
CASL-Junktoren --> Haskell-Junktoren
Terme rekursiv auswerten, Operationen aus der Table nehmen
(siehe CASL.AS_CASL_Basic)
Aufgabe von Shi Hui: XML-Anfragen mit DCC-Ausdr�cken an Bremer Solver schicken
- ggf. Server nutzen
- Vorverarbeitung f�r Solver (z.B. Duplikate raus)
- Shi soll auf Freiburger XML-Format umsteigen (ggf. mit XSLT)
Applikation1 ---
| | -- Freibuger Solver
XML --- |---- Franz�sischer Solver
| |-- Hets -- Bremer Solver
Applikation2 ----- |
ConstraintCASL
|
Semantische Modelle/Korrektheit (CASL, HAsCASL)
XML-Einlesen in Haskell:
HXT (siehe OMDoc.XmlHandling): kann Namespaces
(HaXML: kann Haskell-Datenypen in DTDs umwandeln)
Outline der Diplomarbeit
Qualitative Constraint-Kalk�le (siehe Thomas)
CASL (siehe Paper T. Mossakowski: Relating CASL with Other Specification Languages:
the Institution Level Theoretical Computer Science 286, p. 367-475, 2002.)
CASL-Formeln nur ganz kurz
ConstraintCASL
Signaturen, Signaturmorphismen (aus CASL)
Modelle (aus CASL)
Formeln
Erf�lltheit von Formeln
optional: Erf�lltheitsbedingung
M |= sigma(phi) <=> M|_sigma |= phi
f�r Signaturmorphismus sigma:Sigma_1->Sigma_2
M \in Mod(Sigma_2), phi\in Sen(Sigma_1)
Formalisierung von Kalk�len in ConstraintCASL
Constraint-Solver (auch in ihren Eigenheiten)
�bersetzungen zwischen den verschieden Formaten
praktischer Vergleich
Anwendung
�bersetzungen bis 30.Juni
ConstraintCASL -> Bremer Solver
Bremer Solver -> ConstraintCASL
Parser (mit Parsec), der Kompositionstabelle des Bremer Solvers
parsiert und ConstraintCASL-Spec (abstrakte Syntax) zur�ckgibt
Das kann das als Option in Hets eingebunden werden (Christian Maeder)
Freiburger Constraint-Solver angucken im Juli
�bersetzungen bis 31. Juli
ConstraintCASL -> Freibuger Solver/XML-Format
Option: comptable.xml
Freibuger Solver/XML-Format -> ConstraintCASL
************************************************
Hendrik (Till)
************************************************
OmDoc-Ausgabe konform mit RelaxNG?
OmDoc-Ausgabe Immanual zeigen
Typen von gebundenen Variablen weglassen
XML-Kataloge?
OMDoc-Datentyp einf�hren
Hets <-> Datenstruktur <-> OMDoc
Namensgenerierung/rekonstruktion auf der Seite Hets <-> Datenstruktur
Ursprung von Symbolen bei Hets -> OMDoc: irgendeins nehmen
Ausgabe als DAG, mittels OMR oder ref
Sharing-Algorithmus verwenden
Constraints mit Indizes: ggf. higher-order-Axiom erzeugen (Till fragen)
Anzeigen von lokalen Beweiszielen bei nicht-gesetztem Cons: Till fragen
OMDoc-Bug melden f�r
free type Vehicle ::= sort Boat | sort Car
wobei Boat und Car aus anderen Files kommen
S. 156: Satz einfach streichen
sortdef legt bereits ein Symbol an
werden Signatur-Symbole in OMDoc mit der Theorie versehen, in der
sie als erstes eingef�hrt wurden?
checken f�r Library-Importe
OMDoc/OpenMath-Formeln als Haskell-Datentyp formulieren; diesen als Zwischendatentyp verwenden
Hiding: unterschiedlich in OMDoc und Hets
ein Hets-Hiding-Link mit einer Inklusion Sigma_1->Sigma_2 als
Signaturmorphismus
wird �bersetzt in einen OMDoc-Theoriemorphismus
mit leerer/identischer Abbildung, bei dem die Symbole aus
Sigma_2 \ Sigma_1 versteckt werden
Wenn der Signaturmorphismus keine Inklusion ist, ist keine
�bersetzung m�glich -> Fehler
ein OMDoc-Theoriemorphismus mit Hiding, der eine Inklusion ist
(also leere bzw. identische Abbildung) wird �bersetzt
in einen Hets-Hiding-Link, mit Inklusion als Signaturmorphismus
falls der OMDoc-Theoriemorphismus keine Inklusion ist, muss
ein Hets-Hiding-Link, gefolgt von einem normalen (globalen) Link,
der dann die Umbenennung macht, erzeugt werden
Logiken: �ber verschiedene OMDoc-Theorien mit URI
************************************************
Mingyi (Till)
************************************************
Diplomarbeit
- CASL-Logik: "Relating CASL with other specification languages", S.401-408
- Konservative, definitionale und monomorphe Erweiterungen, Konsistenz
siehe CASL reference manual (suche nach conservative)
- warum sind konservative Erweiterungen wichtig?
- um zu pr�fen, ob Spezifikationen konsistent sind, also implementiert
werden k�nnen
- f�r Refinement-Beweise
- Algorithmen zur Pr�fung von Erweiterungen, ob diese konservativ,
definitional oder monomorph sind
- Beschreibung des Algorithmus in Pseudocode
- Korrektheitsbeweis, d.h. f�r die Erweiterungen, die der Algorithmus
als konservativ erkennt, muss f�r jedes Modell der kleineren
Spezifikation eine Modellerweiterung zur gr��eren Spezifikation
gefunden werden. Z.B. im Falle von free types kann dies eine
Termalgebra-Konstruktion sein.
SP1 -- \sigma --> SP2
konservativ: jedes SP_1-Modell M1 hat eine Erweiterung zu einem
SP2-Modell M2 mit M2|_\sigma=M1.
port CCC to Haskell
Funktionen imageOfMorphism und inhabited
von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
mit "cvs add SigFuns.hs" einchecken
New module FreeTypes.hs:
"free datatypes and recursive equations are consistent"
checkFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
Just True => Yes, is consistent
Just False => No, is inconsistent
Nothing => don't know
call the symbols in the image of the signature morphism "new"
- each new sort must be a free type,
i.e. it must occur in a sort generation constraint that is marked as free
(Sort_gen_ax constrs True)
such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
if not, output "don't know"
and there must be one term of that sort (inhabited)
if not, output "no"
- group the axioms according to their leading operation/predicate symbol,
i.e. the f resp. the p in
forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
Implication Application Strong_equation
forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
Implication Predication Equivalence
if there are axioms not being of this form, output "don't know"
check' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
check' [] = ([([],[])],emptyUniqSet)
-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
check' [EqnInfo n ctx ps (MatchResult CanFail _)]
| all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
check' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
| all_vars ps = (pats, addOneToUniqSet indexs n)
where
(pats,indexs) = check' rs
-- falls ein Konstruktor dabei ist: split_by_constructor
-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
check' qs@((EqnInfo n ctx ps result):_)
| all_vars ps = ([], unitUniqSet n)
| constructors = split_by_constructor qs
| only_vars = first_column_only_vars qs
| otherwise = panic "Check.check': Not implemented :-("
where
-- Note: RecPats will have been simplified to ConPats
-- at this stage.
constructors = or (map is_con qs)
only_vars = and (map is_var qs)
subsort definitions: are conservative if formula is satisfiable
(generate proof obligation)
************************************************
Heng (Klaus)
************************************************
OWL-DL logic
OWL-DL (<)-> CASL-DL
emacs mode:
highlight does not work properly for HasCASL/Set.het or UserManual/Sbcs.casl
some operation symbols
show hets output immediately
C-c C-g for hets -g
when hets terminates abnormally (e.g. with a fail), emacs loops
C-n jumps to the next error, but the message windows is not always scrolled
in such a way that the error is at the top (for long error lists)
Version for XEamcs?
should work with parser error messages as well (adapt these?)
************************************************
Ken (Till)
************************************************
look at command line interface (just call hets)
implement simplified rule Theorem-Hide-Shift
If there is an open global theorem link sigma:N1->N2 and
a hiding definition link theta:N3->N2 (i.e. the signature
morphism theta is from Sig(N2) to Sig(N3)), then prove
this theorem link by inserting a new global theorem link
theta o sigma : N1->N3.
try out examples
conservativity calculus
weakly amalgamable cocones
development graph calculus
(see Sect. IV:4.4 of the CASL Reference Manual)
look at Static/DevGraph.hs
test command line interface (just call hets)
test development graph GUI:
global decomposition
menu edit - unnamed nodes - hide/show nodes,
node menu: show just subtree / undo
interaction with edit - proofs - automatic?
use update of uDrawGraph-nodes,edges instead of erasing and adding nodes
for attribute changes like color
profiling for "automatic" (look at www.haskell.org/ghc)
restrict proofs: only one prove window per node at a given time
************************************************
further task 1
************************************************
generate (x)html code from Doc
generate more readable LaTeX-code
see listings.sty for LaTeX generation (cf. CoSiT paper)
************************************************
further task 2
************************************************
Uni-Refactoring,
make modules hierarchical, replace deprecated code (i.e. FiniteMap, hslibs),
use HaXml as a cabalized library, provide uni as (one?) cabal
package(s), uni used to work under windows as well, watch the
i.e. FilePath, Process discussions (libraries@haskell.org)
possibly switch to a subversion repository, talk to Achim
(amahnke@tzi.de)
************************************************
further task 3
************************************************
look at Static/DevGraph.hs
change management
reload button im Edit-Men� hinzuf�gen (GUI/ConvertAbstractToDevgraph.hs)
reload macht folgendes:
lade CASL-Datei neu ==> neuer Entwicklungsgraph
vergleiche alten+neuen Entwicklungsgraph, konstruiere eine
Abbildung (Common/Lib/Map.hs) von alt nach neu
(jeweils eine Abblidung f�r Knoten und eine f�r Kanten)
Kriterien f�r Finden der Knotenabbildung:
- Namen
- DGOrigin
- Signatur
einfaches Merge von lokalen Beweisen eines abgespeichteren DG
in aktuellen DG
************************************************
further task 4
************************************************
refined graph of Haskell module dependencies
using .import files
************************************************
further task 5
************************************************
port hets to windows. -- costs too much energy at this stage! Till
If hets should become successful then requests for support under
windows will surely follow.
Ghc, uni and uDrawGraph should work under windows. Only Isabelle does
not exist for windows, but SPASS does. Probably only a few path
computations need to be adapted (made modular) within hets. Also
position computations (of Parsec) should be checked under windows.
************************************************
remaining stuff
************************************************
set up a ticket and tracking systems (for bugs and features) instead
of this messy todo list
--> sourceforge???
refactoring of dgraphs: add unique tags + hashes (but no table)
how to compare complex datastructures:
tag x1==tag x2 || (hash x1==hash x2 && x1==x2)
display library graph
(make it really abstract), possibly contact amahnke@tzi.de regarding
Taxonomy, possibly use uni/appl/ontologytool instead of Taxonomy!
set up default simplifier
set up default tactics using axioms
(see DOLCE sample files)
improve efficiency (e.g. of UserManual/Sbcs.casl), using profiling
************************************************
Daniel
************************************************
generate infrastructure for circular coinduction
CCS example: commutativity of || by coinduction
************************************************
Christian
************************************************
Isabelle coding
- improve display syntax in HasCASL-Isabelle coding
- identifiers in mixfix templates must be excluded as ordinary
identifiers (i.e. as quantified variables)
more abstract datatypes?
collect the patches for programatica (or create a package)
- conv (SN i p) = PN i (S p)
+ conv (SN i p) = PN i (Sn (show i) p)
fixes translation error of Pair
simplification of HasCASL sentences (omit types)
Logic COL is a ruin
logic coding from the comand line with printing of results
Haskell modules: hiding, renaming
- group the axioms according to their leading operation/predicate symbol,
i.e. the f resp. the p in
forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
if there are axioms not being of this form, output error
Static analysis for HasCASL
pattern analysis for program equations
implemented only atomic subtyping
Weak amalgamation analysis?
Instantiate Transformation Application system for HasCASL?
Automatic generation of Haskell (for a HasCASL subset)
Proofs in HasCASL
Case study
Coding HasCASL -> Isabelle with definedness axioms
only strict functions are defined
Isabelle interface
One emacs with spec and proof buffer
Reload button should rebuild buffers while keeping as much as possible
keep structuring of Hets theories
************************************************
Rainer (Klaus)
************************************************
SPASS encoding improvements in CASL2SPASS
- if there are predicates defined upon equality substitute them with equality
and remove them from the signature
find definitions (Equivalences) where one side is a binary predicate
and the other side is a builtin equality application (Strong_equation)
return the full qualified (with type) predicate(s)
this is done before the translation of the signature/sentences happens
remove eqPrediate symbols from signature
substitute eqPredications with Strong_equation in the Formulas
implement a catch for calling MathServ based on the catch in runSpass
write just one function that converts Exception to ATPResult
maybe even a specialised catch is useful
such functions fit into Common.Utils or Common.ProofUtils
for the transition to ghc-6.6 spassProve must be corrected
the regexp library changed in functionality
code cleanup and documentation where necessary and possilbe
in SPASS/* and GUI/GenericATP*, GUI/Proofmanagement.hs
************************************************
Klaus
************************************************
for ProofManagement-GUI
mark imported theorems for selection
provide structured (based on spec-names) selection/deselection facility
of axioms and theorems
trace if liniarity of sentences along development is given
for consistency checking with Isabelle, look at the following SAT-Solvers:
MChaff, ZChaff, Berkmin
Consistency checker interface
via global interface, accessible from global and node menus
use falseSentence from Logic.Logic (property: holds in no model)
proved -> inconsistent
disproved -> consistent (assuming completeness)
batch mode for automatic provers such as SPASS
(use automatic flag for provers)
batch interface for Isabelle
each goal is proved separatedly, with a time limit enforced
by killing the process
the tactic is
"using Ax1 ... Axn by auto"
where Ax1 ... Axn is the list of all axioms.
"auto" could be replaced with "best", "blast" etc. (user selection)
Ignore axiom selection for interactive provers
Translation between Achim's ontology data structure and CASL (in Hets)
visualization of "taxonomy" of CASL signatures
(subsorts = inheritance, unary preds = concepts, binary preds = relations)
last two ... partially done
Recognize guarded fragment of CASL:
G ::= forall x . At(x) => G where At is a conjunction of atoms
| exists x . At(x) /\ G
Joost Visser wg. ATerms in Haskell => neues Repository
************************************************
Markus, Lutz
************************************************
Beweise in Isabelle
CASL consistency checker
Weitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
(Vorbild: Larch-Handbuch)
Simpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
Parser and static analysis for CSP-CASL
************************************************
Christoph
************************************************
CASL consistency checker
Integration with generic prover interface?
************************************************
Till
************************************************
duplicate referenced node in SimpleDatatypes.casl
enhance Web interface with SPASS (%implied, consistency)
translation of proofs along comorphisms (it this necessary at all???)
use inverse morphism?
leads to translation of G_theory along comorphism that also
keeps proof status info
this may be used in GUI prover interfaces for recovering old proof attempts
and offering them as default
proveCMDLinteractive (PGIP)
Model expansion flag for comorphisms
Umlaute in daVinci anzeigen
Fragen an Michael:
werden Links in der richtigen Reihenfolge geschrieben (S. 183 OMDoc)?
was ist dort eigentlich das Problem?
Codierung von Subsorten?
paper with Paolo
semantic adequecy of HOL translation
Regulate concurrent proving
.dg files: store only current library; import .dg files for other libraries
Markus' Bsp:
Isabelle: use meta-quantifiers
local subsumption ?
better syntax (Tina)
check for proved theorems
AbstractGraphView: switch to Result monad
unite or rename consCheck and cons_checkers
BinInt.casl: revealing in Int1 does not work correctly
from Stefan W�lfl:
computeTheory does not work across library imports
local theorems
all nodes named
hierarchical Isabelle theories
daVinci printing is not adequate
hiding of internal nodes does not work
CSPs
----
FOL without quantifiers and with uniform disjunctions
(i.e. x R1 y \/ x R2 y)
(with and without =)
algorithmic path consistency over a relation algebra
plug in reasoner for this
develop correctness results (algorithmic path consistency=path consistency)
within CASL
CASL sublogics:
---------------
FOL without quantifiers (with and without =)
guarded fragment
Prop
[from DOLCE cooperation:
quit wish!
ontology mediation via pushouts/pullbacks/pulations
Robinson consistency with shared theory constructed via pre-image?
show theorem links between same instances of different parameterized
specs (where one is an extension of the other one)
link menu for %implies, $def, %cons, even without open proof obligation
for a proved theorem, show minimal part of DG needed for proof
cons, def, mono for nodes
Isabelle interface: each qed should write proof info into file
globally display nodes containing symbols mapped "twice" (i.e. via
different signature morphisms)
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