todo revision 52aad0502f0ddd332a28ae3fcd3327fa66d002f7
afe3ab588a6b2992efe5a9b22ed038545ba3cdbfLennart PoetteringPlan and priority list for CoFI tool activities
b3ae710c251d0ce5cf2cef63208e325497b5e323Zbigniew Jędrzejewski-Szmek************************************************
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers************************************************
f957632b960a0a42999b38ded7089fa602b41745Kay Sieversremove typedecls and op decls generated for datatypes
d19e85f0d474ed1882561b458d528cbae49f640eZbigniew Jędrzejewski-Szmekset up default simplifier
d19e85f0d474ed1882561b458d528cbae49f640eZbigniew Jędrzejewski-Szmekset up default tactics using axioms
d19e85f0d474ed1882561b458d528cbae49f640eZbigniew Jędrzejewski-Szmek************************************************
3e495a6651609d0a45b62aab5c3ed5a3b40e11abZbigniew Jędrzejewski-Szmek************************************************
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poetteringrename variables that conflict with operation syntax
f85857df75cfedbc0d10b8ca2400188dc8f4c22eLennart Poettering (or restrict mixfix decls for consts)
bafb15bab99887d1b6b8a35136531bac6c3876a6Lennart Poetteringdie Mixfix-Deklarationen f�hren noch zu Problemen.
fd6c2363af2cb144bb6a7d6b8bdba9f777440078Lennart Poetteringf�hrt dazu, dass c nicht mehr als Variable verwendet werden kann.
47ee3ee03483efd271642d5043070cbd171f19d4Lennart PoetteringK�nntest du diese Mixfix-Deklarationen auf die notwendigen F�lle
abab50081c8c12cc46482a43264deb46853bb8faLennart Poetteringbeschr�nken, und ggf. die Variablen umbenennen?
abab50081c8c12cc46482a43264deb46853bb8faLennart PoetteringZudem m�ssen Underscores escaped werden:
e6a26d8c972d45a0927ad0b7c654c830daa2243eLennart Poettering C_1::t ("C'_1")
e6a26d8c972d45a0927ad0b7c654c830daa2243eLennart PoetteringDiplom: Encoding for HasCASL in Isabelle/HOL(CF)
e6a26d8c972d45a0927ad0b7c654c830daa2243eLennart PoetteringInterface Hets <-> ISabelle
a2088fd025deb90839c909829e27eece40f7fce4Lennart Poettering Hets muss eine Pipe als Inode erzeugen
a2088fd025deb90839c909829e27eece40f7fce4Lennart Poettering und dann auf Beweisterme warten
a2088fd025deb90839c909829e27eece40f7fce4Lennart Poettering und auf "Ende" warten
a2088fd025deb90839c909829e27eece40f7fce4Lennart Poettering und dann Proof_status sen proof_tree entsprechend ausf�llen
a2088fd025deb90839c909829e27eece40f7fce4Lennart PoetteringIsabelle (im .thy file, dass von IsaProve.hs erzeugt wird)
c874ef05a705d3c679e5fd5a50b81e1f5512c4fdLennart Poettering Beweisterme (siehe Kapitel im RefMan)
c874ef05a705d3c679e5fd5a50b81e1f5512c4fdLennart Poettering ML "proofs := 1" (am Anfang des .thy file)
affb71da79b0c3cbcd6ff6c0cedb218a14162c7cLennart Poettering am Ende jedes Theorems: Beweisterm in die Pipe schreiben
affb71da79b0c3cbcd6ff6c0cedb218a14162c7cLennart Poettering (Pipenamen direkt angeben, vom thy-file-Namen abgeleitet)
affb71da79b0c3cbcd6ff6c0cedb218a14162c7cLennart Poettering mit pretty_proof_of und Pretty.string_of
ff609b8ecd0e36bfff0ba120932307274d993dc8Lennart Poettering und Start- und Endmarker
ff609b8ecd0e36bfff0ba120932307274d993dc8Lennart Poettering am Schluss "Ende" ausgeben
eedb4ac83158bad6f74305612660b4aff6acc6b4Lennart PoetteringFunktion basicInferenceNode in Proofs/Proofs.hs:
de587378ea5d22e11373b18b4fcabf8f26f89529Lennart Poettering Theorem link nur dann gr�n, wenn alle Goals bewiesen wurden
203e81db24ccb9b4dcb0b1bad0ba554116267d20Lennart PoetteringEmacs: uni/emacs, George fragen (ger@)
63432f5d9570b76a8efe82702d69611c20645530Lennart Poettering************************************************
ef6fc8ee57eff8a2b612de0270c9a25e066ee290Lennart Poettering************************************************
47ee3ee03483efd271642d5043070cbd171f19d4Lennart Poettering use save button for saving proof info
c2570ab99be82eddbee0f397fbf8704a95f6f736Lennart Poetteringdevelopment graph calculus
c2570ab99be82eddbee0f397fbf8704a95f6f736Lennart Poettering- Stack overflow for "show just subtree"
c2570ab99be82eddbee0f397fbf8704a95f6f736Lennart Poettering- view-test7.casl should be provable with globDecomp + locDecopm
eba6fd30f2a27f51fa328484cb241807c6934ce1Zbigniew Jędrzejewski-Szmek- fail when doing first globDecomp, then local decomp in RelationsAndOrders
eba6fd30f2a27f51fa328484cb241807c6934ce1Zbigniew Jędrzejewski-Szmek- correct MAYA: glob decomp: some links are not found (Jorina)
eba6fd30f2a27f51fa328484cb241807c6934ce1Zbigniew Jędrzejewski-Szmek- Fail: No match in record selector Static.DevGraph.dgn_sign
c2570ab99be82eddbee0f397fbf8704a95f6f736Lennart Poettering for local subsume in RelationsAndOrders
c2570ab99be82eddbee0f397fbf8704a95f6f736Lennart Poettering************************************************
d89e647542a6ceeefac15fbe8e193de7418bf449Lennart Poettering************************************************
e7e90a8eee056fd12c8ad83470143f7798240dbcLennart Poetteringtype check for CASL
d72bc5973465018e077fcecdcc720840bc1e9cfdLennart Poettering*** Error encode.casl:8.30, No correct typing for
d72bc5973465018e077fcecdcc720840bc1e9cfdLennart Poettering************************************************
d72bc5973465018e077fcecdcc720840bc1e9cfdLennart Poettering************************************************
07cc65c70150faa68a63a444d615f922517c7d94Lennart Poetteringport CCC to Haskell
07cc65c70150faa68a63a444d615f922517c7d94Lennart PoetteringFunktionen imageOfMorphism und inhabited
07cc65c70150faa68a63a444d615f922517c7d94Lennart Poettering von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
07cc65c70150faa68a63a444d615f922517c7d94Lennart Poettering mit "cvs add SigFuns.hs" einchecken
07cc65c70150faa68a63a444d615f922517c7d94Lennart Poettering"free datatypes and recursive equations are consistent"
0a0215783159b9c3a3652b231df36dbff08e0ac5Lennart PoetteringcheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
17978b17d9f5d3591f1c644938efc9c27aa60485Lennart PoetteringJust True => Yes, is consistent
17978b17d9f5d3591f1c644938efc9c27aa60485Lennart PoetteringJust False => No, is inconsistent
17978b17d9f5d3591f1c644938efc9c27aa60485Lennart PoetteringNothing => don't know
17978b17d9f5d3591f1c644938efc9c27aa60485Lennart Poetteringcall the symbols in the image of the signature morphism "new"
48e6d6a6e911af0cf4e3ef12b0a3eeb2c8031d8aLennart Poettering- each new sort must be a free type,
48e6d6a6e911af0cf4e3ef12b0a3eeb2c8031d8aLennart Poettering i.e. it must occur in a sort generation constraint that is marked as free
48e6d6a6e911af0cf4e3ef12b0a3eeb2c8031d8aLennart Poettering (Sort_gen_ax constrs True)
48e6d6a6e911af0cf4e3ef12b0a3eeb2c8031d8aLennart Poettering such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
8aa203819fc7f2a840191f8d9d0e65566c0ce98eLennart Poettering if not, output "don't know"
8aa203819fc7f2a840191f8d9d0e65566c0ce98eLennart Poettering and there must be one term of that sort (inhabited)
b18d23d7ac6a53d52b99dbf0b2048d5a946a2e28Lennart Poettering if not, output "no"
b18d23d7ac6a53d52b99dbf0b2048d5a946a2e28Lennart Poettering- group the axioms according to their leading operation/predicate symbol,
449a22a58f0fa55d9d0fd2eb597272446e032acdLennart Poettering i.e. the f resp. the p in
449a22a58f0fa55d9d0fd2eb597272446e032acdLennart Poettering forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
449a22a58f0fa55d9d0fd2eb597272446e032acdLennart Poettering forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
449a22a58f0fa55d9d0fd2eb597272446e032acdLennart Poettering Implication Application Strong_equation
60d17b74d714fa15d68639062dc2932d7b096229Lennart Poettering forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
60d17b74d714fa15d68639062dc2932d7b096229Lennart Poettering forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
60d17b74d714fa15d68639062dc2932d7b096229Lennart Poettering Implication Predication Equivalence
60d17b74d714fa15d68639062dc2932d7b096229Lennart Poettering if there are axioms not being of this form, output "don't know"
ac749874bbb66c0e7eff15ca35d1616d29b6f3c1Lennart Poetteringcheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
ac749874bbb66c0e7eff15ca35d1616d29b6f3c1Lennart Poetteringcheck' [] = ([([],[])],emptyUniqSet)
7d417f0f357c59cc1846aa832161e69a2328f699Lennart Poettering-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
7d417f0f357c59cc1846aa832161e69a2328f699Lennart Poetteringcheck' [EqnInfo n ctx ps (MatchResult CanFail _)]
e342b74468870f2e4f3e15f7277a0adea42183caZbigniew Jędrzejewski-Szmek | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
e342b74468870f2e4f3e15f7277a0adea42183caZbigniew Jędrzejewski-Szmek-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
036a4773ffa1152e4cabd27473450b8cc01e019bLennart Poetteringcheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
036a4773ffa1152e4cabd27473450b8cc01e019bLennart Poettering | all_vars ps = (pats, addOneToUniqSet indexs n)
036a4773ffa1152e4cabd27473450b8cc01e019bLennart Poettering (pats,indexs) = check' rs
a88abde72169ddc2df77df3fa5bed30725022253Lennart Poettering-- falls ein Konstruktor dabei ist: split_by_constructor
a88abde72169ddc2df77df3fa5bed30725022253Lennart Poettering-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
a88abde72169ddc2df77df3fa5bed30725022253Lennart Poetteringcheck' qs@((EqnInfo n ctx ps result):_)
f93b36affa5ac5710cd84bfb8ff0dafabe99fbf1Lennart Poettering | all_vars ps = ([], unitUniqSet n)
f93b36affa5ac5710cd84bfb8ff0dafabe99fbf1Lennart Poettering | constructors = split_by_constructor qs
20760dcf5df7e253c21a51886cdb02dee612730bLennart Poettering | only_vars = first_column_only_vars qs
20760dcf5df7e253c21a51886cdb02dee612730bLennart Poettering | otherwise = panic "Check.check': Not implemented :-("
20760dcf5df7e253c21a51886cdb02dee612730bLennart Poettering -- Note: RecPats will have been simplified to ConPats
20760dcf5df7e253c21a51886cdb02dee612730bLennart Poettering -- at this stage.
df22b0bbfde403b3fa71f3c2f1e2ca38af946388Lennart Poettering constructors = or (map is_con qs)
df22b0bbfde403b3fa71f3c2f1e2ca38af946388Lennart Poettering only_vars = and (map is_var qs)
c05482281c32bd408808b14c5fb03e706e65602dLennart Poettering************************************************
73cb77549536deab85d8d1261b5381e87d80ab23Lennart Poettering************************************************
477e75ef9ea6bb2e7e8cc76278c442942110f227Lennart Poettering-------------------------------------------------------------------
477e75ef9ea6bb2e7e8cc76278c442942110f227Lennart PoetteringLaTeX pretty printer
7dfb0404b3b6882d582a571f61a52b2f56961675Lennart Poetteringeine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
7dfb0404b3b6882d582a571f61a52b2f56961675Lennart Poetteringund andere Formate besser zu unterst�tzen und einheitlichen PP code
7dfb0404b3b6882d582a571f61a52b2f56961675Lennart Poetteringf�r die CASL Datentypen zu bekommen.
7dfb0404b3b6882d582a571f61a52b2f56961675Lennart PoetteringHasCASL hat auch noch keine Mixfix- und Latex Ausgabe.
2bc39683c0cada86c9dc39e5f3d0ea475cf12e57Lennart Poettering************************************************
687f6a0ba77872299b9fb1f2f04d31c977088a63Lennart Poettering************************************************
687f6a0ba77872299b9fb1f2f04d31c977088a63Lennart Poetteringgenerate infrastructure for circular coinduction
687f6a0ba77872299b9fb1f2f04d31c977088a63Lennart PoetteringCCS example: commutativity of || by coinduction
2bc39683c0cada86c9dc39e5f3d0ea475cf12e57Lennart Poettering************************************************
687f6a0ba77872299b9fb1f2f04d31c977088a63Lennart Poettering************************************************
31a11e8f30449a81867e8fd081e3e76cf6664bb4Lennart Poetteringlogic coding form the comand line with printing of results
dbdee28bfadd6d8bd93cb34c85ce1fc325dd8120Lennart PoetteringHaskell modules: hiding, renaming
17fe56148c44dfa5583a8643c1918fd6eccf2aeeLennart Poettering- group the axioms according to their leading operation/predicate symbol,
17fe56148c44dfa5583a8643c1918fd6eccf2aeeLennart Poettering i.e. the f resp. the p in
17fe56148c44dfa5583a8643c1918fd6eccf2aeeLennart Poettering forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
7687f85ea6bab434324bb985e2898bf6373891bfLennart Poettering forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
7687f85ea6bab434324bb985e2898bf6373891bfLennart Poettering if there are axioms not being of this form, output error
c14db9b32ab90738973071d31f259d1a457d7b4aLennart PoetteringMissing points for heterogeneous WADT 04 example:
c14db9b32ab90738973071d31f259d1a457d7b4aLennart Poettering- improve display of HasCASL sigs + mors
fa607802f332e06f4044c3eb38dbea41076c803dLennart PoetteringStatic analysis for HasCASL
fa607802f332e06f4044c3eb38dbea41076c803dLennart Poettering checking class constraints of terms
a47e6701bfc45519a4e038daa52e9236e932f59aLennart Poettering pattern analysis for program equations
b80c66ba9836456de5260e4a1b696ba25561f613Lennart Poettering - for simple types (currently type synonyms)
bd69054b0987b40a0df87d40772893f6f8a078daLennart Poettering symbol representation
bd69054b0987b40a0df87d40772893f6f8a078daLennart Poettering symbol map analysis (hiding sub/supertypes)
c3a0d00d6dd6f5997d673e133ef6f9f856550b0aLennart PoetteringWeak amalgamation analysis?
c3a0d00d6dd6f5997d673e133ef6f9f856550b0aLennart PoetteringInstantiate Transformation Application system for HasCASL?
c3a0d00d6dd6f5997d673e133ef6f9f856550b0aLennart PoetteringAutomatic generation of Haskell (for a HasCASL subset)
c3a0d00d6dd6f5997d673e133ef6f9f856550b0aLennart PoetteringProofs in HasCASL
de146bb2aac13361ade3050d37696499ac4ca9aeLennart Poettering************************************************
c3a0d00d6dd6f5997d673e133ef6f9f856550b0aLennart Poettering************************************************
d2f81fb00cc3c49e21b31000ba7d37b81a260257Lennart PoetteringCoding of subsorts as unary predicates (for ontologies)
d2f81fb00cc3c49e21b31000ba7d37b81a260257Lennart PoetteringTranslation between Achim's ontology data structure and CASL (in Hets)
b7307642391c8ebb9724c99e6b33239e2c0ff944Lennart Poetteringvisualization of "taxonomy" of CASL signatures
b7307642391c8ebb9724c99e6b33239e2c0ff944Lennart Poettering (subsorts = inheritance, unary preds = concepts, binary preds = relations)
2a441c8afe7c81f74cc2ceccdf9a71301cd39d4dLennart PoetteringRecognize guarded fragment of CASL:
2a441c8afe7c81f74cc2ceccdf9a71301cd39d4dLennart Poettering G ::= forall x . At(x) => G where At is a conjunction of atoms
2a441c8afe7c81f74cc2ceccdf9a71301cd39d4dLennart Poettering | exists x . At(x) /\ G
2a441c8afe7c81f74cc2ceccdf9a71301cd39d4dLennart PoetteringJoost Visser wg. ATerms in Haskell => neues Repository
40ff4a4abd76d71408e598ed02d7860b8465fa9aLennart Poettering************************************************
40ff4a4abd76d71408e598ed02d7860b8465fa9aLennart Poettering************************************************
0a86c1a9d8066267b878dfeddc5e0087dda6a37bLennart PoetteringBeweise in Isabelle
0a86c1a9d8066267b878dfeddc5e0087dda6a37bLennart PoetteringCASL consistency checker
f131770b1465fbf423881f16ba85523a05f846feVeres LajosWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
0a86c1a9d8066267b878dfeddc5e0087dda6a37bLennart Poettering (Vorbild: Larch-Handbuch)
0a86c1a9d8066267b878dfeddc5e0087dda6a37bLennart PoetteringSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
0a86c1a9d8066267b878dfeddc5e0087dda6a37bLennart PoetteringParser and static analysis for CSP-CASL
0a86c1a9d8066267b878dfeddc5e0087dda6a37bLennart Poettering************************************************
0a86c1a9d8066267b878dfeddc5e0087dda6a37bLennart Poettering************************************************
e3286870fdf20c3c93e944b24fd9af53620f7dbaLennart PoetteringCASL consistency checker
e3286870fdf20c3c93e944b24fd9af53620f7dbaLennart PoetteringIsaWin: support CASL-libraries
8514b67754c5ff7fa628929b3d27131010c21842Lennart Poettering************************************************
7b0fce617c48eda32b2d4e04b5f0e4376e8c0106Lennart Poettering************************************************
7b0fce617c48eda32b2d4e04b5f0e4376e8c0106Lennart PoetteringBuffer.het, sublogic of node Buffer:
7b0fce617c48eda32b2d4e04b5f0e4376e8c0106Lennart PoetteringFail: illegal node type in sublogic computation
c2d5b3c94d0c082ef29597fb230f8b88b124bab8Lennart PoetteringJ�rgen Zimmer, Saarbr�cken+Edinburgh, Beweiserkennung f�r versch. Logiken im MathWeb
264b8070715d2d19344c4991ace21147d998f56dLennart Poetteringspec VarTestIncorrect =
f81e67f79fa856aa2ecffad4d014772ce981745cLennart Poettering forall x:t; y:s
6868560773ada8ea31d1f86422be6bf026a1f660Richard Mawspec VarTestCorrect =
758c4d7a391c0e024737053c815bf3924653b8c5Lennart Poettering %% vars x:s; y:t
758c4d7a391c0e024737053c815bf3924653b8c5Lennart Poettering forall x:t; y:s
8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart PoetteringIncorrect geht durch, weil die Typanalyse nicht funktioniert und Correct
8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart Poetteringwird abgelehnt, weil x und y nicht denselben Typ haben, was das richtige
8483d73ff158ee0d51ccbba09a470cc6ae9b071aLennart PoetteringVerhalten auch im ersten Fall w\x{00E4}re.
25e773eeb4f853804e1bf0dbd9a184f23e9b2a97Kay Sieversfor CSP-CASL example: with logic
b857e042d621ffb98a652f33850b431fafbece43Lennart Poetteringheterogeneous static ana
6dab5bb18151c80fc39bd51f03dcff40b920de3eLennart Poetteringtheorem links between nodes in different libraries
384a4be2b00cb95ce215dd343cc9aa77adc9b1ecLennart PoetteringbasicProofs: use info about used axioms
706d97503df83d141d241b645d2c920d691b3d62Lennart Poettering ensure that axiom/thm names are unique
3bcde97e8502c48b53f7420e2433ca68e601662dLennart PoetteringOverload / inlineAxioms: injections
533bb267f13e2f7b4d7b78de30e821dc81c82335Lennart Poetteringremove "prove" menu in abstracted dg
533bb267f13e2f7b4d7b78de30e821dc81c82335Lennart Poetteringbetter sublogic analysis in codings
b42de08aa4c97636e42c28c7bce08f0d7c2a719aZbigniew Jędrzejewski-Szmekthy files in subdir
b42de08aa4c97636e42c28c7bce08f0d7c2a719aZbigniew Jędrzejewski-Szmekadjust path for thy files, such that hets can also be started from subdirs
202aea456dfb279cd34da7bfd1880f6ac0fd849fLennart PoetteringRestrict Sonjas simplifications to HasCASL
42aeb14a4a0fa7d43da96a8ed0fb0e180a2dd5c8Lennart Poetteringadd suitable axioms to simplifier and CR
42aeb14a4a0fa7d43da96a8ed0fb0e180a2dd5c8Lennart PoetteringcomputeTheory: remove double axioms
42aeb14a4a0fa7d43da96a8ed0fb0e180a2dd5c8Lennart Poetteringadd suitable axioms to simplifier and classical reasoner
6868560773ada8ea31d1f86422be6bf026a1f660Richard Mawbetter display of internal nodes (use tooltip?)
14a32924c9b46817c92ae11c1147a59dcb62012bLennart Poetteringupdate Hets, CASL, daVinci on web page
563b1bdc09efe0cf94dd3f514f30376ca854c1ceLennart PoetteringCASL2PCFOL: x_i -> t_i, t=[inj(x_i)]
5dcf983854c2e8314dbee239180255490ec8ae1cLennart Poetteringpacking of binaries: add hets-update, refer to TclTk
6bd7941ece602ae9962a103c8d65ecda7d642391Tom Gundersentest for sublogic before applying comorphism
510cc5ae0810d71e167cc5b389d36995f90e29cfTom GundersenMissing points for heterogeneous WADT 04 example:
510cc5ae0810d71e167cc5b389d36995f90e29cfTom Gundersen- coding to Isabelle: translate sort gen constraints
ed220efd6657822332b9563ec53c5ab9f3c33220Lennart Poettering- Improve adapation to Isabelle's lexis
41488fe9024a8955d19811620fd55dcc56a5b2baLennart PoetteringIsabelle: (ask Christoph)
41488fe9024a8955d19811620fd55dcc56a5b2baLennart Poettering remove datatypes from sort list
41488fe9024a8955d19811620fd55dcc56a5b2baLennart Poettering prove local thm link (=> green)
41488fe9024a8955d19811620fd55dcc56a5b2baLennart Poettering "prove" menu with choice windows
1dbe0a6efda7b1d35957eab7e1d56a2c69d806d9Lennart Poettering incorporate sublogics
1dbe0a6efda7b1d35957eab7e1d56a2c69d806d9Lennart Poettering sublogic translation table
157a180e4fc827606833a6724834ba7b0246d650Tom Gundersen better interaction between Isabelle instance (for one node)
823f4a91ebd8942a2c1ff31050dc55eaa60f6ffcLukas Nykryn + selection of single goals that are proved
510cc5ae0810d71e167cc5b389d36995f90e29cfTom Gundersen => use PGIP interface (Christoph, David)
b873d33ec9583c92a0c2bc6807d010720fa31595Lennart Poettering correct show theory
9d6db739ce1eaa3eace21801fd606d523b73c8f4Lennart Poettering Keep proofs and lemmas in .thy files (kind of merge)
1dbe0a6efda7b1d35957eab7e1d56a2c69d806d9Lennart Poettering CASL-like syntax
1dbe0a6efda7b1d35957eab7e1d56a2c69d806d9Lennart Poettering CASL annotation for lemmas that should be used in proof
9d6db739ce1eaa3eace21801fd606d523b73c8f4Lennart Poettering inherit CASL's mixfix syntax
23c4091dc2b85d117512e89233fdeb47d1ff3d92Lennart PoetteringSignatures versus theories: where to store additional infos?
9d6db739ce1eaa3eace21801fd606d523b73c8f4Lennart Poetteringcomp(id,x)=x for comorphism names
9d6db739ce1eaa3eace21801fd606d523b73c8f4Lennart PoetteringGeneralise CASL2Modal
bc07548926ec5ed7b13df8d3656654f238e0b9a7Lennart PoetteringMixfix analysis + typecheck for modality axiomatizations
17018c3cc7ba3dcb4e6aeb8a77203b08fd09f726Tom GundersenModal logics: modal logic, temporal logic, mu calculus
17018c3cc7ba3dcb4e6aeb8a77203b08fd09f726Tom Gundersen+ translations (e.g. modal to FOL)
b6b63571ae3eca1741d54172922961af972b8f20Lennart PoetteringCASL->Haskell with free DTs (mark sortgens) + recursion
e2a69298819b58f008be61d314f8ab95ccaec427Lennart Poettering- List[Dec] wird List[Pos]
2834ffe78d7fd8be118429aa1449ac72641638c2Lennart Poettering- George wg. Schlie�en von Fenstern
2834ffe78d7fd8be118429aa1449ac72641638c2Lennart Poettering- node numbers do not match
a940778fb1dd16479f455bab3ac6cbdbc5b06165Lennart Poettering- thm links with external target should be provable as well
3c779fa59d1825d7db2a9516669d34ded7916913Lennart PoetteringRemove warnings
a01647e53727107d82382bc5c9d98c894e8f386cLennart PoetteringDifferent types of logic translations
3de03738fc970496d2d3da668c72767a48ccc41bLennart PoetteringImprove Static analysis of structured specs
3de03738fc970496d2d3da668c72767a48ccc41bLennart PoetteringDevelopment graph calculus, Strategies for DG rules
2b1c3767515672dfd0f5e0a9c9d7ac3a16a6a361Lennart PoetteringManagement of change
37efac5ddb21fd91ed420c070ed07f375e78b3b9Lennart PoetteringIntegrate provers
37efac5ddb21fd91ed420c070ed07f375e78b3b9Lennart Poettering Otter model checker
7348b3adb324614132cf376f478e883bd7de28f1Lennart Poettering FOL-prover by Uli Furhbach
7348b3adb324614132cf376f478e883bd7de28f1Lennart Poettering modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
e107ed185ef08945102834234a05ec51bb438685Lennart Poettering Isabelle codings: www.inf.ethz.ch/~vigano
e107ed185ef08945102834234a05ec51bb438685Lennart Poettering Renate Schmidt, Manchester: uses FOL prover for description logic
81429136905a6204875174b60a179333b7f3c9e4Kay Sievers (as efficient as DL-specific tools!)
81429136905a6204875174b60a179333b7f3c9e4Kay Sievers Look at PROSPER toolkit
e107ed185ef08945102834234a05ec51bb438685Lennart Poettering consistency: see IJCAR-workshop on non-provability in Cork
f598ac3e28b729dd0b1d0a881df3e16465687a2bLennart Poettering IJCAR workshop about logical frameworks and meta-languages
769918ecd30c0f7ee6e87b9aa6226d956bd2f530Lennart PoetteringKlaus' wayfinding example
769918ecd30c0f7ee6e87b9aa6226d956bd2f530Lennart Poetteringask Detlef: critical pairs, Fossacs paper by Francesco
6a3f892a23db71544d0439355f96c44350dafa8fLennart PoetteringUniForM workbench:
2a781fc9bd33982c81e5ff75974a442a33d4f167Lennart Poetteringfirst steps towards CASL instance, using ATerms and re-using MMISS instance
2a781fc9bd33982c81e5ff75974a442a33d4f167Lennart Poetteringvariants for specs (needed for DOLCE: CASL variant, DL variant, ...)
6a3f892a23db71544d0439355f96c44350dafa8fLennart PoetteringIntegration of MAYA and Isabelle/HOL (global HOL-Coding of
650264033f2f98f6319513958d94d59078654af8Lennart Poettering Grothendieck logic)
650264033f2f98f6319513958d94d59078654af8Lennart Poettering + for TAS: reflection of HOL in HOL, to be composed with encodings
650264033f2f98f6319513958d94d59078654af8Lennart Poettering (i.e. signatures, axioms, signature morphisms in HOL,
f8901862b2b030921b3d5aba4157044ceab16451Lennart Poettering re-use ML signatures) (Einar)
eda8f06755bd98c4639293c26b856c225f0d1fe1Lennart PoetteringDisplay Specs as daVinci subgraphs
af1082b04a3d45a9b1d796b4271f44e87e307026Lennart PoetteringLogic graph window
af1082b04a3d45a9b1d796b4271f44e87e307026Lennart PoetteringInput text window
af1082b04a3d45a9b1d796b4271f44e87e307026Lennart PoetteringDevelopment graph window
488ad3b32a7e2b5b1380abf4a15e5f65fa65f3feLennart Poettering************************************************
488ad3b32a7e2b5b1380abf4a15e5f65fa65f3feLennart Poettering************************************************
47c94a96df29080f8b3a97e7362df4e9c6ba3265Lennart PoetteringHets 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)
47c94a96df29080f8b3a97e7362df4e9c6ba3265Lennart PoetteringPackaging of installation
09ecd746c9d6581664873674c2188f8c93ed7780Lennart Poettering with Eclipse, WXHaskell or GTk?
09ecd746c9d6581664873674c2188f8c93ed7780Lennart Poettering how to integrate with event system of UniForM workbench?
09ecd746c9d6581664873674c2188f8c93ed7780Lennart Poetteringintegrate graphviz (or use Java interface for racer? or Isabelle browser? or...?)
09ecd746c9d6581664873674c2188f8c93ed7780Lennart Poettering this interacts with GUI!
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart PoetteringData.Serizable (only when ghc supports it)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poetteringincrease performance
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poetteringintegrate QuickCheck: come to lecture!
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering++++++++++++++++++++++++++++++++++++++++++++++++
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart PoetteringRemaining things
0bee65f0622c4faa8ac8ae771cc0c8a936dfa284Lennart Poettering++++++++++++++++++++++++++++++++++++++++++++++++
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart PoetteringMark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering Coq, PTT in Maude
47c94a96df29080f8b3a97e7362df4e9c6ba3265Lennart PoetteringProofs with basic datatypes
718db96199eb307751264e4163555662c9a389faLennart PoetteringVerbesserung der Fehlermeldungen
718db96199eb307751264e4163555662c9a389faLennart PoetteringImprove encoding: CATS/basic_encode.sml (3 days)
718db96199eb307751264e4163555662c9a389faLennart PoetteringMore HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
718db96199eb307751264e4163555662c9a389faLennart PoetteringRenamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)
966204e010ed432a1d7a0481d41a326d8ec7b0c8Lennart PoetteringExample of Agnes und Frank: proofs in HOL-CASL (2 days)
966204e010ed432a1d7a0481d41a326d8ec7b0c8Lennart PoetteringTerm input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
94676f3e9352cbf1f72e0a512ee0d2ed83ff676dLennart PoetteringExamples for cond rewriting -> Christophe
6fd4d0209827e5c3e52fa8c7144852f550f8f95cLennart PoetteringDoku: VSE-Prover, VSE-Method VSE-demo in Bremen?
416446221d905b6815175dc4d525d27f8ae43d1bLennart PoetteringAdapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
416446221d905b6815175dc4d525d27f8ae43d1bLennart PoetteringEigene IsaWin-Instanz mit CASL-RS statt HOL-RS
7f79cd7109a60810140a045cc725291fc5515264Lennart PoetteringHOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)
0aafd43d235982510d1c40564079f7bcec0c7c19Lennart PoetteringHOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)
19aadacf92ad86967ffb678e37b2ff9e83cb9480Jan EngelhardtHOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)
19aadacf92ad86967ffb678e37b2ff9e83cb9480Jan EngelhardtEncoding of structured free (3 days)
df5f6971e6e15b4632884916c71daa076c8bae96Lennart PoetteringEncoding of structured cofree (2 weeks)
df5f6971e6e15b4632884916c71daa076c8bae96Lennart PoetteringEingabesyntax als Mix zwischen CASL und HOL (3 days)
fcba531ed4c6e6f8f21d8ca4e3a56e3162b1c578Lennart PoetteringAdapt Isabelle unions to CASL unions (1 week)
fcba531ed4c6e6f8f21d8ca4e3a56e3162b1c578Lennart PoetteringIsaWin git/src/isa_ext/casl_thy.sml (1 week)
6aaa8c2f783cd1b3ac27c5ce40625d032e7e3d71Zbigniew Jędrzejewski-SzmekGenerate Proof obligations (1 week)
c3bb87dbab8b79bb9253407cb5b7f3e6fe8db395Lennart PoetteringAdd renaming to Isabelle kernel (2 months)
bdeeb6b543a2a2d0a494f17b85f1498859cdfc2fLennart PoetteringRepository mit korrekten und fehlerhaften Specs
bdeeb6b543a2a2d0a494f17b85f1498859cdfc2fLennart PoetteringHetCATS User manual, Doku fuer Environments (2 weeks)
4e09014daf8f98584b3f15e64e93bed232e70a6bLennart PoetteringConversion ASF/SDF-Parser -> abstract syntax (in Haskell)
4e09014daf8f98584b3f15e64e93bed232e70a6bLennart PoetteringComparsion of parsers (ML-yacc parser, SDF-Parser)
6bb648a16ae4a682ad4784412af706d2e6a3e4daTom GundersenConversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren
0d43ffef5ad277183ebaef259b2210bfaf913749Lennart PoetteringPVS anbinden (Kooperation mit Cachan?)
d0928791499734e202460d5c027b5d3e0d28e7abLennart PoetteringPortations: Intel-Solaris, Mac OS-10 (2 weeks)
7212c6083a5577eabc96c35c9db4c19c113cae93Lennart Poettering(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm
57f2a947270faf65e1876797b930e3f6d60ebd06Lennart PoetteringViews on CASL specs: CATS/viewer.sml (2 weeks)
d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan EngelhardtUebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart PoetteringModule graph CATS/module_graph.sml (1 week) -> Maya?
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart PoetteringATerms via XML: CATS/aterms.sml (2 weeks)
80caea6cc72ebd311a311b1527cc6b87201c13bfLennart PoetteringNeues Tool-Schaubild auf Web-Seiten ver�ffentlichen
df98a87ba389bdfc0359beedf47557411f3af434Lennart PoetteringLibrary management: CATS/lib_ana.sml (2 weeks)
df98a87ba389bdfc0359beedf47557411f3af434Lennart PoetteringVersion management/Uniform Workbench: CATS/lib_ana.sml (2 months)
69727e6dc69ae5d9b5ae3681723778a3faa354e9Lennart Poettering{- This does not work due to needed ordering:
279f036675536d55c901562b49f9df146af1a0e3Lennart Poetteringinstance Functor Set where
279f036675536d55c901562b49f9df146af1a0e3Lennart Poetteringinstance Monad Set where
279f036675536d55c901562b49f9df146af1a0e3Lennart Poettering return = unitSet
b568ef14a75dffb7182e0acbdec743b31df2a597Lennart Poettering m >>= k = unionManySets (setToList (fmap k m))
eb01ba5de14859d7a94835ab9299de40132d549aLennart PoetteringAufbau von comptable
154ff088d371bee5651eaa2bc9bde8a34c185656Lennart Poettering--------------------
154ff088d371bee5651eaa2bc9bde8a34c185656Lennart Poettering[("normal","normal","normal"),
154ff088d371bee5651eaa2bc9bde8a34c185656Lennart Poettering ("normal","inclusion","normal"),
154ff088d371bee5651eaa2bc9bde8a34c185656Lennart Poettering ("inclusion","normal","normal"),
69af45035913e7119cffd94c542bd3039600e45dZbigniew Jędrzejewski-Szmek ("inclusion","inclusion","inclusion")]
461bd8e47cafacfcd38389e7558330bfb6e902adLennart PoetteringAufbau von ginfo
461bd8e47cafacfcd38389e7558330bfb6e902adLennart Poettering--------------------
461bd8e47cafacfcd38389e7558330bfb6e902adLennart PoetteringMit initgraphs erzeugen
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart PoetteringAufbau des Graphen selbst
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart Poettering------------------------