todo revision 0b54df32e275652e0d01cf0b16d2401377526539
afe3ab588a6b2992efe5a9b22ed038545ba3cdbfLennart PoetteringPlan and priority list for CoFI tool activities
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers************************************************
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers************************************************
a40593a0d0d740efa387e35411e1e456a6c5aba7Lennart PoetteringDiplom: Encoding for HasCASL in Isabelle/HOL(CF)
afe3ab588a6b2992efe5a9b22ed038545ba3cdbfLennart PoetteringInterface Hets <-> ISabelle
d19e85f0d474ed1882561b458d528cbae49f640eZbigniew Jędrzejewski-Szmek Hets muss eine Pipe als Inode erzeugen
d19e85f0d474ed1882561b458d528cbae49f640eZbigniew Jędrzejewski-Szmek und dann auf Beweisterme warten
d19e85f0d474ed1882561b458d528cbae49f640eZbigniew Jędrzejewski-Szmek und auf "Ende" warten
3f85ef0f05ffc51e19f86fb83a1c51e8e3cd6817Harald Hoyer und dann Proof_status sen proof_tree entsprechend ausf�llen
afea8d3853d0f76b3845729ff00e75d281f43a1bZbigniew Jędrzejewski-SzmekIsabelle (im .thy file, dass von IsaProve.hs erzeugt wird)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering Beweisterme (siehe Kapitel im RefMan)
f85857df75cfedbc0d10b8ca2400188dc8f4c22eLennart Poettering ML "proofs := 1" (am Anfang des .thy file)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering am Ende jedes Theorems: Beweisterm in die Pipe schreiben
bafb15bab99887d1b6b8a35136531bac6c3876a6Lennart Poettering (Pipenamen direkt angeben, vom thy-file-Namen abgeleitet)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering mit pretty_proof_of und Pretty.string_of
bafb15bab99887d1b6b8a35136531bac6c3876a6Lennart Poettering und Start- und Endmarker
81429136905a6204875174b60a179333b7f3c9e4Kay Sievers am Schluss "Ende" ausgeben
58f55364fa00a6a4706df2c4a01c6967f432e531Lennart PoetteringFunktion basicInferenceNode in Proofs/Proofs.hs:
83a1ff25e5228b0a5b2cc942fd4f964d10bb73b0Zbigniew Jędrzejewski-Szmek Theorem link nur dann gr�n, wenn alle Goals bewiesen wurden
83a1ff25e5228b0a5b2cc942fd4f964d10bb73b0Zbigniew Jędrzejewski-SzmekEmacs: uni/emacs, George fragen (ger@)
83a1ff25e5228b0a5b2cc942fd4f964d10bb73b0Zbigniew Jędrzejewski-Szmek************************************************
81429136905a6204875174b60a179333b7f3c9e4Kay SieversJorina (Till)
fbe1a1a94f19112d7e5d60c40d87487ad24e2ce4Lennart Poettering************************************************
8514b67754c5ff7fa628929b3d27131010c21842Lennart Poetteringdevelopment graph calculus
6c78f43c7b0e54e695af49917fda79b584f46830Lennart Poettering- Stack overflow for "show just subtree"
6c78f43c7b0e54e695af49917fda79b584f46830Lennart Poettering- view-test7.casl should be provable with globDecomp + locDecopm
7b0fce617c48eda32b2d4e04b5f0e4376e8c0106Lennart Poettering- fail when doing first globDecomp, then local decomp in RelationsAndOrders
7b0fce617c48eda32b2d4e04b5f0e4376e8c0106Lennart Poettering- correct MAYA: glob decomp: some links are not found (Jorina)
7b0fce617c48eda32b2d4e04b5f0e4376e8c0106Lennart Poettering************************************************
b568ef14a75dffb7182e0acbdec743b31df2a597Lennart Poettering************************************************
264b8070715d2d19344c4991ace21147d998f56dLennart Poetteringtype check for CASL
7e27f3121e5a10629302b5221eb21345f832724aLennart Poettering*** Error encode.casl:8.30, No correct typing for
f81e67f79fa856aa2ecffad4d014772ce981745cLennart Poettering************************************************
d48b7bd271b1e70924c8485d2f95c2f5a1ae77cbLennart Poettering************************************************
25e14499c4c5b02229d05a5bc26c3693ade5f987Lennart Poetteringport CCC to Haskell
758c4d7a391c0e024737053c815bf3924653b8c5Lennart PoetteringFunktionen imageOfMorphism und inhabited
821cc13ddae40fb7608458b44aaa7a3fd33d56d9Lennart Poettering von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
821cc13ddae40fb7608458b44aaa7a3fd33d56d9Lennart Poettering mit "cvs add SigFuns.hs" einchecken
8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart Poettering"free datatypes and recursive equations are consistent"
8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart PoetteringcheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart PoetteringJust True => Yes, is consistent
8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart PoetteringJust False => No, is inconsistent
8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart PoetteringNothing => don't know
b857e042d621ffb98a652f33850b431fafbece43Lennart Poetteringcall the symbols in the image of the signature morphism "new"
6dab5bb18151c80fc39bd51f03dcff40b920de3eLennart Poettering- each new sort must be a free type,
384a4be2b00cb95ce215dd343cc9aa77adc9b1ecLennart Poettering i.e. it must occur in a sort generation constraint that is marked as free
384a4be2b00cb95ce215dd343cc9aa77adc9b1ecLennart Poettering (Sort_gen_ax constrs True)
706d97503df83d141d241b645d2c920d691b3d62Lennart Poettering such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
706d97503df83d141d241b645d2c920d691b3d62Lennart Poettering if not, output "don't know"
3bcde97e8502c48b53f7420e2433ca68e601662dLennart Poettering and there must be one term of that sort (inhabited)
3bcde97e8502c48b53f7420e2433ca68e601662dLennart Poettering if not, output "no"
533bb267f13e2f7b4d7b78de30e821dc81c82335Lennart Poettering- group the axioms according to their leading operation/predicate symbol,
533bb267f13e2f7b4d7b78de30e821dc81c82335Lennart Poettering i.e. the f resp. the p in
279f036675536d55c901562b49f9df146af1a0e3Lennart Poettering forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
533bb267f13e2f7b4d7b78de30e821dc81c82335Lennart Poettering forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
202aea456dfb279cd34da7bfd1880f6ac0fd849fLennart Poettering Implication Application Strong_equation
202aea456dfb279cd34da7bfd1880f6ac0fd849fLennart Poettering forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
42aeb14a4a0fa7d43da96a8ed0fb0e180a2dd5c8Lennart Poettering forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
42aeb14a4a0fa7d43da96a8ed0fb0e180a2dd5c8Lennart Poettering Implication Predication Equivalence
42aeb14a4a0fa7d43da96a8ed0fb0e180a2dd5c8Lennart Poettering if there are axioms not being of this form, output "don't know"
14a32924c9b46817c92ae11c1147a59dcb62012bLennart Poetteringcheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
14a32924c9b46817c92ae11c1147a59dcb62012bLennart Poetteringcheck' [] = ([([],[])],emptyUniqSet)
563b1bdc09efe0cf94dd3f514f30376ca854c1ceLennart Poettering-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
563b1bdc09efe0cf94dd3f514f30376ca854c1ceLennart Poetteringcheck' [EqnInfo n ctx ps (MatchResult CanFail _)]
5dcf983854c2e8314dbee239180255490ec8ae1cLennart Poettering | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
5dcf983854c2e8314dbee239180255490ec8ae1cLennart Poettering-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
b873d33ec9583c92a0c2bc6807d010720fa31595Lennart Poetteringcheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
d61bb44a89fde3042c7c15ea4975239f7dcb0cb0Lennart Poettering | all_vars ps = (pats, addOneToUniqSet indexs n)
ed220efd6657822332b9563ec53c5ab9f3c33220Lennart Poettering (pats,indexs) = check' rs
41488fe9024a8955d19811620fd55dcc56a5b2baLennart Poettering-- falls ein Konstruktor dabei ist: split_by_constructor
41488fe9024a8955d19811620fd55dcc56a5b2baLennart Poettering-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
41488fe9024a8955d19811620fd55dcc56a5b2baLennart Poetteringcheck' qs@((EqnInfo n ctx ps result):_)
41488fe9024a8955d19811620fd55dcc56a5b2baLennart Poettering | all_vars ps = ([], unitUniqSet n)
41488fe9024a8955d19811620fd55dcc56a5b2baLennart Poettering | constructors = split_by_constructor qs
41488fe9024a8955d19811620fd55dcc56a5b2baLennart Poettering | only_vars = first_column_only_vars qs
41488fe9024a8955d19811620fd55dcc56a5b2baLennart Poettering | otherwise = panic "Check.check': Not implemented :-("
ca70bec9261977336c94f44d5fcf37e1c495326aLennart Poettering -- Note: RecPats will have been simplified to ConPats
ca70bec9261977336c94f44d5fcf37e1c495326aLennart Poettering -- at this stage.
1dbe0a6efda7b1d35957eab7e1d56a2c69d806d9Lennart Poettering constructors = or (map is_con qs)
1dbe0a6efda7b1d35957eab7e1d56a2c69d806d9Lennart Poettering only_vars = and (map is_var qs)
b873d33ec9583c92a0c2bc6807d010720fa31595Lennart Poettering************************************************
1dbe0a6efda7b1d35957eab7e1d56a2c69d806d9Lennart Poettering************************************************
9d6db739ce1eaa3eace21801fd606d523b73c8f4Lennart PoetteringTranslation from CASL with partiality to CASL without partiality
ff3d6560bead6879a2fed1bf99bfe8273b3723f1Zbigniew Jędrzejewski-Szmekdetails: see paper in Theoretical Computer Science, p. 418
23c4091dc2b85d117512e89233fdeb47d1ff3d92Lennart Poettering************************************************
0f47ed0a052c0da743404f23ac3532aaabd23655Lennart Poettering************************************************
bc07548926ec5ed7b13df8d3656654f238e0b9a7Lennart PoetteringWrite web interface for Hets
b6b63571ae3eca1741d54172922961af972b8f20Lennart Poetteringsee the web interface for Cats:
279f036675536d55c901562b49f9df146af1a0e3Lennart Poetteringhttp://www.informatik.uni-bremen.de/cgi-bin/cats.cgi
e2a69298819b58f008be61d314f8ab95ccaec427Lennart Poettering/home/till/www/cgi-bin/cats.cgi, adapt for Hets
e2a69298819b58f008be61d314f8ab95ccaec427Lennart Poettering(replace name of binary: /home/cofi/bin/hets -w ,
2834ffe78d7fd8be118429aa1449ac72641638c2Lennart Poettering replace string
2834ffe78d7fd8be118429aa1449ac72641638c2Lennart Poettering put hets.cgi to /home/jiang/www/cgi-bin/hets.cgi
a940778fb1dd16479f455bab3ac6cbdbc5b06165Lennart Poettering test with www.tzi.de/cgiwrap/jiang/hets.cgi )
3c779fa59d1825d7db2a9516669d34ded7916913Lennart PoetteringAdd option -w to Hets (hetcats/Options.hs)
a940778fb1dd16479f455bab3ac6cbdbc5b06165Lennart Poetteringin hets.hs, look for option, if present, proceed URL input
a01647e53727107d82382bc5c9d98c894e8f386cLennart Poetteringtranslate GUI/WebInterface.hs to Haskell
37efac5ddb21fd91ed420c070ed07f375e78b3b9Lennart Poettering - output parse tree
37efac5ddb21fd91ed420c070ed07f375e78b3b9Lennart Poettering - output pretty printed ASCII
7348b3adb324614132cf376f478e883bd7de28f1Lennart Poettering - output pretty printed LaTeX
7348b3adb324614132cf376f478e883bd7de28f1Lennart Poettering - output development graph (needs GraphBrowser.class, see
e107ed185ef08945102834234a05ec51bb438685Lennart Poettering http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/HOL/medium.html)
01083ad094664e5c685060f4fb35a05ea2f212edLennart Poettering-------------------------------------------------------------------
edb2935c5c5b95c42b8679086f60da5eafad74cbLennart PoetteringLaTeX pretty printer
769918ecd30c0f7ee6e87b9aa6226d956bd2f530Lennart Poetteringa) analysierte Formeln und Terme optimal/k�rzer ausgeben:
6a3f892a23db71544d0439355f96c44350dafa8fLennart Poetteringshorten :: Sign -> {TERM, FORMULA} -> {TERM, FORMULA}
2a781fc9bd33982c81e5ff75974a442a33d4f167Lennart PoetteringIn Abh�ngigkeit von Sign werden z.B. nicht-�berladene Funktionen
6a3f892a23db71544d0439355f96c44350dafa8fLennart Poetteringunqualifiziert ausgeben bzw. zwecks Eindeutigkeit wird (minimal) nur
6a3f892a23db71544d0439355f96c44350dafa8fLennart Poetteringmit dem Ergebnistyp qualifiziert.
650264033f2f98f6319513958d94d59078654af8Lennart Poettering((a: Nat) + (b: Nat)): Nat
f8901862b2b030921b3d5aba4157044ceab16451Lennart Poetteringb) eine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
eda8f06755bd98c4639293c26b856c225f0d1fe1Lennart Poetteringund andere Formate besser zu unterst�tzen und einheitlichen PP code
eda8f06755bd98c4639293c26b856c225f0d1fe1Lennart Poetteringf�r die CASL Datentypen zu bekommen.
d4fdc205a4610965cee46408dbd046c922e7620cLennart PoetteringHasCASL hat auch noch keine Mixfix- und Latex Ausgabe.
af1082b04a3d45a9b1d796b4271f44e87e307026Lennart Poettering************************************************
af1082b04a3d45a9b1d796b4271f44e87e307026Lennart Poettering************************************************
488ad3b32a7e2b5b1380abf4a15e5f65fa65f3feLennart PoetteringHaskell modules: hiding, renaming
488ad3b32a7e2b5b1380abf4a15e5f65fa65f3feLennart Poettering- group the axioms according to their leading operation/predicate symbol,
488ad3b32a7e2b5b1380abf4a15e5f65fa65f3feLennart Poettering i.e. the f resp. the p in
488ad3b32a7e2b5b1380abf4a15e5f65fa65f3feLennart Poettering forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
47c94a96df29080f8b3a97e7362df4e9c6ba3265Lennart Poettering forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
47c94a96df29080f8b3a97e7362df4e9c6ba3265Lennart Poettering if there are axioms not being of this form, output error
09ecd746c9d6581664873674c2188f8c93ed7780Lennart PoetteringMissing points for heterogeneous WADT 04 example:
09ecd746c9d6581664873674c2188f8c93ed7780Lennart Poettering- improve display of HasCASL sigs + mors
09ecd746c9d6581664873674c2188f8c93ed7780Lennart PoetteringStatic analysis for HasCASL
09ecd746c9d6581664873674c2188f8c93ed7780Lennart Poettering checking class constraints of terms
ef417cfd2211ae017a38b9796c6db29130133e63Zbigniew Jędrzejewski-Szmek pattern analysis for program equations
3333d748facc15f49935b6b793490ba0824976e6Zbigniew Jędrzejewski-Szmek - for simple types (currently type synonyms)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering symbol representation
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering symbol map analysis (hiding sub/supertypes)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart PoetteringWeak amalgamation analysis?
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart PoetteringInstantiate Transformation Application system for HasCASL?
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart PoetteringAutomatic generation of Haskell (for a HasCASL subset)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart PoetteringProofs in HasCASL
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering************************************************
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering************************************************
47c94a96df29080f8b3a97e7362df4e9c6ba3265Lennart Poetteringvisualization of "taxonomy" of CASL signatures
47c94a96df29080f8b3a97e7362df4e9c6ba3265Lennart Poettering (subsorts = inheritance, unary preds = concepts, binary preds = relations)
718db96199eb307751264e4163555662c9a389faLennart PoetteringRecognize guarded fragment of CASL:
718db96199eb307751264e4163555662c9a389faLennart Poettering G ::= forall x . At(x) => G where At is a conjunction of atoms
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering | exists x . At(x) /\ G
718db96199eb307751264e4163555662c9a389faLennart PoetteringJoost Visser wg. ATerms in Haskell => neues Repository
718db96199eb307751264e4163555662c9a389faLennart Poettering************************************************
966204e010ed432a1d7a0481d41a326d8ec7b0c8Lennart Poettering************************************************
6fd4d0209827e5c3e52fa8c7144852f550f8f95cLennart PoetteringBeweise in Isabelle
416446221d905b6815175dc4d525d27f8ae43d1bLennart PoetteringCASL consistency checker
416446221d905b6815175dc4d525d27f8ae43d1bLennart PoetteringWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
7f79cd7109a60810140a045cc725291fc5515264Lennart Poettering (Vorbild: Larch-Handbuch)
0aafd43d235982510d1c40564079f7bcec0c7c19Lennart PoetteringSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
19aadacf92ad86967ffb678e37b2ff9e83cb9480Jan EngelhardtParser and static analysis for CSP-CASL
df5f6971e6e15b4632884916c71daa076c8bae96Lennart Poettering************************************************
fcba531ed4c6e6f8f21d8ca4e3a56e3162b1c578Lennart Poettering************************************************
6aaa8c2f783cd1b3ac27c5ce40625d032e7e3d71Zbigniew Jędrzejewski-SzmekCASL consistency checker
c3bb87dbab8b79bb9253407cb5b7f3e6fe8db395Lennart PoetteringIsaWin: support CASL-libraries
18d4e7c26e7806ac363d19989df7144d5058ce41Lennart Poettering************************************************
bdeeb6b543a2a2d0a494f17b85f1498859cdfc2fLennart Poettering************************************************
bdeeb6b543a2a2d0a494f17b85f1498859cdfc2fLennart PoetteringStatic analysis of architectural specs
4e09014daf8f98584b3f15e64e93bed232e70a6bLennart Poettering************************************************
6bb648a16ae4a682ad4784412af706d2e6a3e4daTom Gundersen************************************************
7212c6083a5577eabc96c35c9db4c19c113cae93Lennart PoetteringCASL2PCFOL: x_i -> t_i, t=[inj(x_i)]
7212c6083a5577eabc96c35c9db4c19c113cae93Lennart Poetteringpacking of binaries: add hets-update, refer to TclTk
7212c6083a5577eabc96c35c9db4c19c113cae93Lennart Poetteringtest for sublogic before applying comorphism
9398f650939aec0d44ea7d20240502cafd667c29Lennart Poetteringavoid cyclic comorphisms
d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan EngelhardtMissing points for heterogeneous WADT 04 example:
7973ca1927e1f3bac9438f3529458c9ff868905dLennart Poettering- coding to Isabelle: translate sort gen constraints
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering- extended globDecomp rule: existing local Thm links
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering (e.g. generated by %implied) should lead to fewer new local
dc17bcef197a0d5ee798cce59c40e4f5e85c24f6Lennart Poettering links ("local composition" rule)
ab9716c2489f9141ed13ec22dbb216b3e6fbd6b5Lennart Poettering- Improve adapation to Isabelle's lexis
df98a87ba389bdfc0359beedf47557411f3af434Lennart PoetteringIsabelle: (ask Christoph)
df98a87ba389bdfc0359beedf47557411f3af434Lennart Poettering free datatypes
df98a87ba389bdfc0359beedf47557411f3af434Lennart Poettering prove local thm link (=> green)
6a8b5fa4635ed858788fb10099ec9b62b3359a0aLennart Poettering "prove" menu with choice windows
69727e6dc69ae5d9b5ae3681723778a3faa354e9Lennart Poettering incorporate sublogics
279f036675536d55c901562b49f9df146af1a0e3Lennart Poettering sublogic translation table
279f036675536d55c901562b49f9df146af1a0e3Lennart Poettering better interaction between Isabelle instance (for one node)
279f036675536d55c901562b49f9df146af1a0e3Lennart Poettering + selection of single goals that are proved
b568ef14a75dffb7182e0acbdec743b31df2a597Lennart Poettering => use PGIP interface (Christoph, David)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering correct show theory
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering Keep proofs and lemmas in .thy files (kind of merge)
12179984a38fe74581333fbcdc11c822d81f505fLennart Poettering CASL-like syntax
0536ce5d0ceaf87f3e81faaff41d69ffeed2186fZbigniew Jędrzejewski-Szmek CASL annotation for lemmas that should be used in proof
eb01ba5de14859d7a94835ab9299de40132d549aLennart Poettering inherit CASL's mixfix syntax
154ff088d371bee5651eaa2bc9bde8a34c185656Lennart PoetteringSignatures versus theories: where to store additional infos?
154ff088d371bee5651eaa2bc9bde8a34c185656Lennart Poetteringcomp(id,x)=x for comorphism names
e8a7a315391a6a07897122725cd707f4e9ce63d7Lennart PoetteringGeneralise CASL2Modal
461bd8e47cafacfcd38389e7558330bfb6e902adLennart PoetteringMixfix analysis + typecheck for modality axiomatizations
461bd8e47cafacfcd38389e7558330bfb6e902adLennart PoetteringModal logics: modal logic, temporal logic, mu calculus
461bd8e47cafacfcd38389e7558330bfb6e902adLennart Poettering+ translations (e.g. modal to FOL)
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart PoetteringCASL->Haskell with free DTs (mark sortgens) + recursion
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart PoetteringCoding of subsorts as unary predicates (for ontologies)
b454b11220e87add6d0f011695c7912b009c853dLennart PoetteringTranslation between Achim's ontology data structure and CASL (in Hets)
4ff49cb63075aba646b578f2516b37a8dfd5a65bLennart Poettering- List[Dec] wird List[Pos]
4ff49cb63075aba646b578f2516b37a8dfd5a65bLennart Poettering- George wg. Schlie�en von Fenstern
fff87a35d9e26c0d4ea41273a963c0eb20e18da4Zbigniew Jędrzejewski-Szmek- node numbers do not match
fff87a35d9e26c0d4ea41273a963c0eb20e18da4Zbigniew Jędrzejewski-Szmek- thm links with external target should be provable as well
b8b4d3dddc7611dce3bf28004b0375d661120c62Lennart PoetteringRemove warnings
d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan EngelhardtDifferent types of logic translations
b5c03638d48c07aa0eaf13b5f54000c7133e1883Lennart PoetteringImprove Static analysis of structured specs
b5c03638d48c07aa0eaf13b5f54000c7133e1883Lennart PoetteringDevelopment graph calculus, Strategies for DG rules
b5c03638d48c07aa0eaf13b5f54000c7133e1883Lennart PoetteringManagement of change
eece8c6fb5f4d354dcef6fd369e876c4f3a3f163Lennart PoetteringIntegrate provers
eece8c6fb5f4d354dcef6fd369e876c4f3a3f163Lennart Poettering Otter model checker
356ce9915ab1a4a1e6dc26954df34936a69e7c12Lennart Poettering FOL-prover by Uli Furhbach
356ce9915ab1a4a1e6dc26954df34936a69e7c12Lennart Poettering modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
09f727eebd87661f263d3c2c1e0de7b7771acd40Lennart Poettering Isabelle codings: www.inf.ethz.ch/~vigano
09f727eebd87661f263d3c2c1e0de7b7771acd40Lennart Poettering Renate Schmidt, Manchester: uses FOL prover for description logic
09f727eebd87661f263d3c2c1e0de7b7771acd40Lennart Poettering (as efficient as DL-specific tools!)
c144692179098c1861f2aeafc67689a74439cf4cLennart Poettering Look at PROSPER toolkit
c144692179098c1861f2aeafc67689a74439cf4cLennart Poettering consistency: see IJCAR-workshop on non-provability in Cork
c144692179098c1861f2aeafc67689a74439cf4cLennart Poettering IJCAR workshop about logical frameworks and meta-languages
0be8342c04bbf129b4a21e5073eacccbbce4e896Lennart PoetteringKlaus' wayfinding example
e5ec62c56963d997edaffa904af5dc45dac23988Lennart PoetteringUniForM workbench:
54c31a79f72ff57ac8eba089acacc4ab482b745dLennart Poetteringfirst steps towards CASL instance, using ATerms and re-using MMISS instance
826872b61e4857dfffe63ba84e2b005623baecd6Lennart Poetteringvariants for specs (needed for DOLCE: CASL variant, DL variant, ...)
d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan EngelhardtIntegration of MAYA and Isabelle/HOL (global HOL-Coding of
826872b61e4857dfffe63ba84e2b005623baecd6Lennart Poettering Grothendieck logic)
3679d1126bae52e02f6cd60fca196f616b9e660dLennart Poettering + for TAS: reflection of HOL in HOL, to be composed with encodings
3679d1126bae52e02f6cd60fca196f616b9e660dLennart Poettering (i.e. signatures, axioms, signature morphisms in HOL,
3679d1126bae52e02f6cd60fca196f616b9e660dLennart Poettering re-use ML signatures) (Einar)
3679d1126bae52e02f6cd60fca196f616b9e660dLennart PoetteringDisplay Specs as daVinci subgraphs
81d112a8f0522a09fcfe317f420363a2b728137cLennart PoetteringLogic graph window
490b7e47093d491a2bdb1084fe92b796f4e07eefLennart PoetteringInput text window
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringDevelopment graph window
e41814846c19a48f4490169d82e359e005c4db45Lennart Poettering************************************************
e9fd44b728ff1fc0d1f24fccb87a767f6865df27Lennart Poettering************************************************
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringHets Web interface (cf. CATS/web_interface2.sml)
3040728b6691ea2e9df3a2060e2d49a792bbaedaLennart PoetteringPackaging of installation
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringintegrate QuickCheck
e6c6e7afffa80ad74efdb1ddfa815294624f1608Lennart Poetteringincrease performance
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering++++++++++++++++++++++++++++++++++++++++++++++++
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringRemaining things
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering++++++++++++++++++++++++++++++++++++++++++++++++
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringMark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
e5ec62c56963d997edaffa904af5dc45dac23988Lennart Poettering Coq, PTT in Maude
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart PoetteringProof general interface (1 day)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart PoetteringTest Maya with basic datatypes
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart PoetteringVerbesserung der Fehlermeldungen
279f036675536d55c901562b49f9df146af1a0e3Lennart PoetteringImprove encoding: CATS/basic_encode.sml (3 days)
279f036675536d55c901562b49f9df146af1a0e3Lennart PoetteringMore HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
279f036675536d55c901562b49f9df146af1a0e3Lennart PoetteringRenamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)
279f036675536d55c901562b49f9df146af1a0e3Lennart PoetteringExample of Agnes und Frank: proofs in HOL-CASL (2 days)
279f036675536d55c901562b49f9df146af1a0e3Lennart PoetteringTerm input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
279f036675536d55c901562b49f9df146af1a0e3Lennart PoetteringExamples for cond rewriting -> Christophe
279f036675536d55c901562b49f9df146af1a0e3Lennart PoetteringDoku: VSE-Prover, VSE-Method VSE-demo in Bremen?
279f036675536d55c901562b49f9df146af1a0e3Lennart PoetteringAdapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
279f036675536d55c901562b49f9df146af1a0e3Lennart PoetteringEigene IsaWin-Instanz mit CASL-RS statt HOL-RS
279f036675536d55c901562b49f9df146af1a0e3Lennart PoetteringHOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)
279f036675536d55c901562b49f9df146af1a0e3Lennart PoetteringHOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)
b568ef14a75dffb7182e0acbdec743b31df2a597Lennart PoetteringHOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart PoetteringEncoding of structured free (3 days)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringEncoding of structured cofree (2 weeks)
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart PoetteringEingabesyntax als Mix zwischen CASL und HOL (3 days)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringAdapt Isabelle unions to CASL unions (1 week)
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart PoetteringIsaWin git/src/isa_ext/casl_thy.sml (1 week)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringGenerate Proof obligations (1 week)
57f2a947270faf65e1876797b930e3f6d60ebd06Lennart PoetteringAdd renaming to Isabelle kernel (2 months)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringRepository mit korrekten und fehlerhaften Specs
d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan EngelhardtHetCATS User manual, Doku fuer Environments (2 weeks)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringConversion ASF/SDF-Parser -> abstract syntax (in Haskell)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringComparsion of parsers (ML-yacc parser, SDF-Parser)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringConversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringPVS anbinden (Kooperation mit Cachan?)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringPortations: Intel-Solaris, Mac OS-10 (2 weeks)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringViews on CASL specs: CATS/viewer.sml (2 weeks)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringUebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringModule graph CATS/module_graph.sml (1 week) -> Maya?
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringATerms via XML: CATS/aterms.sml (2 weeks)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringNeues Tool-Schaubild auf Web-Seiten ver�ffentlichen
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringLibrary management: CATS/lib_ana.sml (2 weeks)
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringVersion management/Uniform Workbench: CATS/lib_ana.sml (2 months)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering{- This does not work due to needed ordering:
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poetteringinstance Functor Set where
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poetteringinstance Monad Set where
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering return = unitSet
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering m >>= k = unionManySets (setToList (fmap k m))
279f036675536d55c901562b49f9df146af1a0e3Lennart PoetteringAufbau von comptable
279f036675536d55c901562b49f9df146af1a0e3Lennart Poettering--------------------
279f036675536d55c901562b49f9df146af1a0e3Lennart Poettering[("normal","normal","normal"),
279f036675536d55c901562b49f9df146af1a0e3Lennart Poettering ("normal","inclusion","normal"),
279f036675536d55c901562b49f9df146af1a0e3Lennart Poettering ("inclusion","normal","normal"),
279f036675536d55c901562b49f9df146af1a0e3Lennart Poettering ("inclusion","inclusion","inclusion")]
279f036675536d55c901562b49f9df146af1a0e3Lennart PoetteringAufbau von ginfo
279f036675536d55c901562b49f9df146af1a0e3Lennart Poettering--------------------
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart PoetteringMit initgraphs erzeugen
8b8f259170e35b93e6c6d1757cb8b835bbdaa40cZbigniew Jędrzejewski-SzmekAufbau des Graphen selbst
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering------------------------