todo revision 0317c2ef1c222f6664e9b494d10c68ee2114475e
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringPlan and priority list for CoFI tool activities
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringImmanuel
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringSuchfunktion f�r einen Knoten im DG:
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering welche anderen Knoten sind hier mit Theoriemorphismus abbildbar?
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering erstmal auf eine Logik (z.B. CASL) beschr�nken
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering - Funktion f�r Morphismus-Suche zwischen Theorien
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering - evtl. angucken: CASL.SymbolMapAnalysis, inducedFromToMorphism Map.empty
5430f7f2bc7330f3088b894166bf3524a067e3d8Lennart Poettering RawSymbolMap als "Suche-Guide" wird erestzt durch Axiome/Theoreme
5430f7f2bc7330f3088b894166bf3524a067e3d8Lennart Poettering - Einbindung ins GUI (GUI.ConvertAbstractToDevGraph)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringBasicProof in Proofs.Proofs: sind Datenstrukturen f�r informelle Beweise OK?
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringKonfidenzgrade von Beweisen?
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringvon Till/HiWi zu erledigen:
5430f7f2bc7330f3088b894166bf3524a067e3d8Lennart PoetteringRepr�sentation �ndern:
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Beweisobjekte an DGs, nicht an Regeln -- done
5430f7f2bc7330f3088b894166bf3524a067e3d8Lennart Poettering F�r Theoreme in Theorien an Beweisobjekte -- done
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering BasicProof mit Liste von Beweisobjekten -- �berfl�ssig
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Definitionen auszeichnen -- done
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering F�r alles siehe G_theory, ThSens und SenStatus.
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Isabelles Beweisobjekte einbinden
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringFlorian (Till)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringabstrakte Syntax f�r ConstraintCASL (s. CASL-lib/ConstraintCASL/)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering nach HetCATS/ConstraintCASL/AS_ConstraintCASL.der.hs
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Range hinzuf�gen (vgl. HetCATS/CASL/AS_Basic.der.hs)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringParser f�r ConstraintCASL
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering nach HetCATS/ConstraintCASL/Parse_AS_Basic.hs
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering tokens aus Common/Lexer.hs wiederverwenden
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering neuer Parser f�r Terme
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringTesten mit
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering hets -o ast.het CASL-lib/ConstraintCASL/RCC8.het
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering trace verwenden
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering einfachen Test einchecken
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringFreiburger Constraint-Solver angucken
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringBremer Constraint-Solver angucken
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringMingyi (Till)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringport CCC to Haskell
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringFunktionen imageOfMorphism und inhabited
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering mit "cvs add SigFuns.hs" einchecken
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringNew module FreeTypes.hs:
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering"free datatypes and recursive equations are consistent"
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringcheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringJust True => Yes, is consistent
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringJust False => No, is inconsistent
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringNothing => don't know
9f7dad774ebfad23269800b7096eaad087481debVille Skyttä
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringcall the symbols in the image of the signature morphism "new"
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering- each new sort must be a free type,
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering i.e. it must occur in a sort generation constraint that is marked as free
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering (Sort_gen_ax constrs True)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering if not, output "don't know"
4f755fc6ab8b75f89ed84c93cd5c3fac2a448b16Lennart Poettering and there must be one term of that sort (inhabited)
4f755fc6ab8b75f89ed84c93cd5c3fac2a448b16Lennart Poettering if not, output "no"
4f755fc6ab8b75f89ed84c93cd5c3fac2a448b16Lennart Poettering- group the axioms according to their leading operation/predicate symbol,
4f755fc6ab8b75f89ed84c93cd5c3fac2a448b16Lennart Poettering i.e. the f resp. the p in
4f755fc6ab8b75f89ed84c93cd5c3fac2a448b16Lennart Poettering forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
4f755fc6ab8b75f89ed84c93cd5c3fac2a448b16Lennart Poettering forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Implication Application Strong_equation
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Implication Predication Equivalence
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering if there are axioms not being of this form, output "don't know"
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringcheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringcheck' [] = ([([],[])],emptyUniqSet)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringcheck' [EqnInfo n ctx ps (MatchResult CanFail _)]
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringcheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering | all_vars ps = (pats, addOneToUniqSet indexs n)
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering where
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering (pats,indexs) = check' rs
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering-- falls ein Konstruktor dabei ist: split_by_constructor
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringcheck' qs@((EqnInfo n ctx ps result):_)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering | all_vars ps = ([], unitUniqSet n)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering | constructors = split_by_constructor qs
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering | only_vars = first_column_only_vars qs
2b583ce6576d4a074ce6f1570b3e60b65c64ae7dKay Sievers | otherwise = panic "Check.check': Not implemented :-("
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering where
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering -- Note: RecPats will have been simplified to ConPats
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering -- at this stage.
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering constructors = or (map is_con qs)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering only_vars = and (map is_var qs)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
9f7dad774ebfad23269800b7096eaad087481debVille Skyttä
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringsubsort definitions: are conservative if formula is satisfiable
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering (generate proof obligation)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
9980033377c105d2cd6539c9d73ee61d4c2263b0Lennart Poettering************************************************
9980033377c105d2cd6539c9d73ee61d4c2263b0Lennart PoetteringHeng (Klaus)
9980033377c105d2cd6539c9d73ee61d4c2263b0Lennart Poettering************************************************
9980033377c105d2cd6539c9d73ee61d4c2263b0Lennart Poettering
9980033377c105d2cd6539c9d73ee61d4c2263b0Lennart PoetteringOWL-DL logic
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringOWL-DL (<)-> CASL-DL
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringemacs mode:
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering highlight does not work properly for HasCASL/Set.het or UserManual/Sbcs.casl
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering some operation symbols
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering show hets output immediately
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering C-c C-g for hets -g
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering when hets terminates abnormally (e.g. with a fail), emacs loops
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering C-n jumps to the next error, but the message windows is not always scrolled
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering in such a way that the error is at the top (for long error lists)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Version for XEamcs?
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering should work with parser error messages as well (adapt these?)
a41fe3a29372f8e6c4e7733bf85940a023811301Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringHilfskraft 1
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringModal-CASL <-> CASL-DL
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering see Chapter 4 of "The Description Logic Handbook"
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering and ask Klaus for a print out of it
ab1f063390f55e14a8de87f21c4fad199eb908a6Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringHilfskraft 2
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringUni-Refactoring,
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringmake modules hierarchical, change scoped type variables for ghc-6.5
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering(and older ghcs), replace deprecated code (i.e. FiniteMap, hslibs),
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poetteringuse HaXml as a cabalized library, provide uni as (one?) cabal
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poetteringpackage(s), uni used to work under windows as well, watch the
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poetteringi.e. FilePath, Process discussions (libraries@haskell.org)
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poettering
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poetteringpossibly switch to a subversion repository, talk to Achim
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poettering(amahnke@tzi.de)
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poettering
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poettering
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poettering************************************************
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart PoetteringKen (Till)
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocil************************************************
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocil
4f755fc6ab8b75f89ed84c93cd5c3fac2a448b16Lennart Poetteringdevelopment graph calculus
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocil(see Sect. IV:4.4 of the CASL Reference Manual)
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocil
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocillook at Static/DevGraph.hs
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocillook at Proofs/EdgeUtils.hs Proofs/StatusUtils.hs Proofs/Global.hs
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocil
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocilimplement simplified rule Theorem-Hide-Shift
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskociltry out examples
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocilconservativity calculus
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocilweakly amalgamable cocones
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocil
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poettering************************************************
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart PoetteringZheng (Till)
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poettering************************************************
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poettering
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poetteringlook at Static/DevGraph.hs
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poetteringlook at translation to OMDoc
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poettering
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poetteringchange management via translation to OMDoc
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poettering
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poetteringeinfaches Merge von lokalen Beweisen eines abgespeichteren DG
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poettering in aktuellen DG
40c32a4ad488256e934ce9ecc05ebfac04851711Léo Gillot-Lamure
40c32a4ad488256e934ce9ecc05ebfac04851711Léo Gillot-Lamure************************************************
40c32a4ad488256e934ce9ecc05ebfac04851711Léo Gillot-LamureHilfskraft 4
40c32a4ad488256e934ce9ecc05ebfac04851711Léo Gillot-Lamure************************************************
40c32a4ad488256e934ce9ecc05ebfac04851711Léo Gillot-Lamure
0cd1fd4369685b10953ada832a0b505f5732667dPierre Schmitzport hets to windows.
40c32a4ad488256e934ce9ecc05ebfac04851711Léo Gillot-Lamure
40c32a4ad488256e934ce9ecc05ebfac04851711Léo Gillot-LamureIf hets should become successful then requests for support under
40c32a4ad488256e934ce9ecc05ebfac04851711Léo Gillot-Lamurewindows will surely follow.
40c32a4ad488256e934ce9ecc05ebfac04851711Léo Gillot-Lamure
a41fe3a29372f8e6c4e7733bf85940a023811301Lennart PoetteringGhc, uni and uDrawGraph should work under windows. Only Isabelle does
ff01d048b4c1455241c894cf7982662c9d28fd34Lennart Poetteringnot exist for windows, but SPASS does. Probably only a few path
a41fe3a29372f8e6c4e7733bf85940a023811301Lennart Poetteringcomputations need to be adapted (made modular) within hets. Also
a41fe3a29372f8e6c4e7733bf85940a023811301Lennart Poetteringposition computations (of Parsec) should be checked under windows.
a41fe3a29372f8e6c4e7733bf85940a023811301Lennart Poettering
a41fe3a29372f8e6c4e7733bf85940a023811301Lennart Poettering************************************************
a41fe3a29372f8e6c4e7733bf85940a023811301Lennart PoetteringHilfskraft 5
a41fe3a29372f8e6c4e7733bf85940a023811301Lennart Poettering************************************************
a41fe3a29372f8e6c4e7733bf85940a023811301Lennart Poettering
a41fe3a29372f8e6c4e7733bf85940a023811301Lennart Poetteringrefactor pretty printing
bc2f673ec24b59948fcfc35b3077fda0314e69d8Lennart Poettering
bc2f673ec24b59948fcfc35b3077fda0314e69d8Lennart Poetteringeine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
bc2f673ec24b59948fcfc35b3077fda0314e69d8Lennart Poetteringund andere Formate besser zu unterst�tzen und einheitlichen PP code
bc2f673ec24b59948fcfc35b3077fda0314e69d8Lennart Poettering(independent from GlobalAnnos) f�r die (Het-)CASL (and HasCASL!)
bc2f673ec24b59948fcfc35b3077fda0314e69d8Lennart PoetteringDatentypen (particularly for HasCASL data types) zu bekommen.
bc2f673ec24b59948fcfc35b3077fda0314e69d8Lennart Poettering
bc2f673ec24b59948fcfc35b3077fda0314e69d8Lennart PoetteringLaTeX: see listings.sty for LaTeX generation (cf. CoSiT paper)
bc2f673ec24b59948fcfc35b3077fda0314e69d8Lennart Poettering
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering************************************************
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poetteringremaining stuff
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering************************************************
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poetteringset up a ticket and tracking systems (for bugs and features) instead
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poetteringof this messy todo list
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering--> sourceforge???
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poetteringrefactoring of dgraphs: add unique tags (but no table)
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poetteringdisplay library graph
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poetteringunify GUI/AbstractGraphView.hs and Taxonomy/AbstractGraphView.hs
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poetteringand uni/appl/ontologytool/AbstractGraphView.hs
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering(make it really abstract), possibly contact amahnke@tzi.de regarding
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart PoetteringTaxonomy, possibly use uni/appl/ontologytool instead of Taxonomy!
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poetteringset up default simplifier
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poetteringset up default tactics using axioms
d87be9b0af81a6e07d4fb3028e45c4409100dc26Lennart Poettering (see DOLCE sample files)
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poetteringimprove efficiency (e.g. of UserManual/Sbcs.casl), using profiling
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poetteringdevelopment graph calculus
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering- Stack overflow for "show just subtree"
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering- view-test7.casl should be provable with globDecomp + locDecopm
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering- fail when doing first globDecomp, then local decomp in RelationsAndOrders
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering- correct MAYA: glob decomp: some links are not found (Jorina)
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering- Fail: No match in record selector Static.DevGraph.dgn_sign
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering for local subsume in RelationsAndOrders
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering************************************************
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart PoetteringDaniel
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering************************************************
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-Szmekgenerate infrastructure for circular coinduction
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-SzmekCCS example: commutativity of || by coinduction
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-Szmek************************************************
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-SzmekChristian
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-Szmek************************************************
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-Szmek
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-Szmekcollect the patches for programatica (or create a package)
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-Szmek- conv (SN i p) = PN i (S p)
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-Szmek+ conv (SN i p) = PN i (Sn (show i) p)
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poetteringin programatica/tools/base/parse2/NumberNames.hs
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-Szmekfixes translation error of Pair
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-Szmek
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poetteringsimplification of HasCASL sentences (omit types)
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-Szmek
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-SzmekLogic COL is a ruin (with wrongly qualified module names)
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-Szmek
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-Szmeklogic coding from the comand line with printing of results
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-Szmek
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart PoetteringHaskell modules: hiding, renaming
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-Szmek- group the axioms according to their leading operation/predicate symbol,
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering i.e. the f resp. the p in
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering if there are axioms not being of this form, output error
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart PoetteringMissing points for heterogeneous WADT 04 example:
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering- improve display of HasCASL sigs + mors
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart PoetteringStatic analysis for HasCASL
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering pattern analysis for program equations
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering implemented only atomic subtyping
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringWeak amalgamation analysis?
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringInstantiate Transformation Application system for HasCASL?
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringAutomatic generation of Haskell (for a HasCASL subset)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringProofs in HasCASL
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart PoetteringCase study
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart PoetteringRainer (Klaus)
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering************************************************
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart PoetteringConnecting Hets with MathServ
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Either use
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering - haifa (http://www.dcs.shef.ac.uk/~simonf/HAIFA.html)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering pros: * relies not on external tool
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering * light weight call
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering cons: * code is not well maintained
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering * a lot of the deserialization of the answer must be done
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering in Haskell
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering - call a java program included in MathServ distrib
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering pros: * works imediately
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering * deserilisation is mostly done in java
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering cons: * use of external tool
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Use modified dfg2tptp to translate SPASS theories into TPTP problems
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering (ask Klaus for sources)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Add possibility to choose a prover out of a list of available provers
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering (similar to "More fine grained..." and behind more fine grained)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Adapt Comorphisms.KnownProvers to select a certain prover at the end of a
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering comorphism automatically
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Adapt existing SPASS GUI to cover call of the MathServ broker
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering by - transforming the grid layout packer into the packer
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering used in GUI.ProofManagement (easier to maintain and to extend)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering - abstraction of certain parts of the GUI into helper functions
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering forms a new generic Prover-GUI toolkit
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering - on top of this GUI toolkit
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering Write a GUI based on the generic Prover-GUI
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering to call MathServ's Vampire service directly
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering with additional parameters
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering
************************************************
Klaus
************************************************
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
allgemeine Hets-GUI
f�r Anzeige von (un)bewiesenen Goals, ... done
bewiesene Goals als Axioms mit ausgeben ... was ist das ???
das ist schon implementiert ("Theorems to include if proven")
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
IsaWin: support CASL-libraries
************************************************
Till
************************************************
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
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