todo revision 52aad0502f0ddd332a28ae3fcd3327fa66d002f7
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPlan and priority list for CoFI tool activities
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski************************************************
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder************************************************
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederremove typedecls and op decls generated for datatypes
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiset up default simplifier
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskiset up default tactics using axioms
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski************************************************
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski************************************************
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederrename variables that conflict with operation syntax
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (or restrict mixfix decls for consts)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederdie Mixfix-Deklarationen f�hren noch zu Problemen.
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederf�hrt dazu, dass c nicht mehr als Variable verwendet werden kann.
5e46b572ed576c0494768998b043d9d340594122Till MossakowskiK�nntest du diese Mixfix-Deklarationen auf die notwendigen F�lle
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangbeschr�nken, und ggf. die Variablen umbenennen?
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaederZudem m�ssen Underscores escaped werden:
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang C_1::t ("C'_1")
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaederDiplom: Encoding for HasCASL in Isabelle/HOL(CF)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederInterface Hets <-> ISabelle
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Hets muss eine Pipe als Inode erzeugen
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder und dann auf Beweisterme warten
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich und auf "Ende" warten
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder und dann Proof_status sen proof_tree entsprechend ausf�llen
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus LuettichIsabelle (im .thy file, dass von IsaProve.hs erzeugt wird)
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich Beweisterme (siehe Kapitel im RefMan)
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich ML "proofs := 1" (am Anfang des .thy file)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder am Ende jedes Theorems: Beweisterm in die Pipe schreiben
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (Pipenamen direkt angeben, vom thy-file-Namen abgeleitet)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski mit pretty_proof_of und Pretty.string_of
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder und Start- und Endmarker
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder am Schluss "Ende" ausgeben
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederFunktion basicInferenceNode in Proofs/Proofs.hs:
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski Theorem link nur dann gr�n, wenn alle Goals bewiesen wurden
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederEmacs: uni/emacs, George fragen (ger@)
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder************************************************
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder************************************************
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder use save button for saving proof info
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederdevelopment graph calculus
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder- Stack overflow for "show just subtree"
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder- view-test7.casl should be provable with globDecomp + locDecopm
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder- fail when doing first globDecomp, then local decomp in RelationsAndOrders
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder- correct MAYA: glob decomp: some links are not found (Jorina)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder- Fail: No match in record selector Static.DevGraph.dgn_sign
4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maeder for local subsume in RelationsAndOrders
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder************************************************
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski************************************************
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maedertype check for CASL
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder*** Error encode.casl:8.30, No correct typing for
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder************************************************
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder************************************************
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederport CCC to Haskell
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiFunktionen imageOfMorphism und inhabited
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder mit "cvs add SigFuns.hs" einchecken
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder"free datatypes and recursive equations are consistent"
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaedercheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaederJust True => Yes, is consistent
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaederJust False => No, is inconsistent
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaederNothing => don't know
26d11a256b1433604a3dbc69913b520fff7586acChristian Maedercall the symbols in the image of the signature morphism "new"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder- each new sort must be a free type,
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder i.e. it must occur in a sort generation constraint that is marked as free
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (Sort_gen_ax constrs True)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder if not, output "don't know"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder and there must be one term of that sort (inhabited)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder if not, output "no"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder- group the axioms according to their leading operation/predicate symbol,
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder i.e. the f resp. the p in
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Implication Application Strong_equation
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Implication Predication Equivalence
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder if there are axioms not being of this form, output "don't know"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedercheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedercheck' [] = ([([],[])],emptyUniqSet)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedercheck' [EqnInfo n ctx ps (MatchResult CanFail _)]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskicheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder | all_vars ps = (pats, addOneToUniqSet indexs n)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (pats,indexs) = check' rs
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder-- falls ein Konstruktor dabei ist: split_by_constructor
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maedercheck' qs@((EqnInfo n ctx ps result):_)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder | all_vars ps = ([], unitUniqSet n)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder | constructors = split_by_constructor qs
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder | only_vars = first_column_only_vars qs
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder | otherwise = panic "Check.check': Not implemented :-("
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder -- Note: RecPats will have been simplified to ConPats
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -- at this stage.
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder constructors = or (map is_con qs)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder only_vars = and (map is_var qs)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski************************************************
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski************************************************
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederOWL-DL -> CASL
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-------------------------------------------------------------------
26d11a256b1433604a3dbc69913b520fff7586acChristian MaederLaTeX pretty printer
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskieine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiund andere Formate besser zu unterst�tzen und einheitlichen PP code
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskif�r die CASL Datentypen zu bekommen.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiHasCASL hat auch noch keine Mixfix- und Latex Ausgabe.
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder************************************************
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski************************************************
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedergenerate infrastructure for circular coinduction
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiCCS example: commutativity of || by coinduction
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski************************************************
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder************************************************
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederlogic coding form the comand line with printing of results
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederHaskell modules: hiding, renaming
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder- group the axioms according to their leading operation/predicate symbol,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski i.e. the f resp. the p in
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder if there are axioms not being of this form, output error
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederMissing points for heterogeneous WADT 04 example:
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder- improve display of HasCASL sigs + mors
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederStatic analysis for HasCASL
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder checking class constraints of terms
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder pattern analysis for program equations
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder - for simple types (currently type synonyms)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder symbol representation
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder symbol map analysis (hiding sub/supertypes)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederWeak amalgamation analysis?
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederInstantiate Transformation Application system for HasCASL?
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederAutomatic generation of Haskell (for a HasCASL subset)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederProofs in HasCASL
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder************************************************
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski************************************************
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederCoding of subsorts as unary predicates (for ontologies)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederTranslation between Achim's ontology data structure and CASL (in Hets)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maedervisualization of "taxonomy" of CASL signatures
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder (subsorts = inheritance, unary preds = concepts, binary preds = relations)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederRecognize guarded fragment of CASL:
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder G ::= forall x . At(x) => G where At is a conjunction of atoms
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder | exists x . At(x) /\ G
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederJoost Visser wg. ATerms in Haskell => neues Repository
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder************************************************
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder************************************************
0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian MaederBeweise in Isabelle
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederCASL consistency checker
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder (Vorbild: Larch-Handbuch)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederParser and static analysis for CSP-CASL
0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian Maeder************************************************
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder************************************************
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiCASL consistency checker
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiIsaWin: support CASL-libraries
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder************************************************
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder************************************************
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederBuffer.het, sublogic of node Buffer:
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederFail: illegal node type in sublogic computation
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederJ�rgen Zimmer, Saarbr�cken+Edinburgh, Beweiserkennung f�r versch. Logiken im MathWeb
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maederspec VarTestIncorrect =
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder vars x:s; y:t
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder forall x:t; y:s
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maederspec VarTestCorrect =
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder %% vars x:s; y:t
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder forall x:t; y:s
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederIncorrect geht durch, weil die Typanalyse nicht funktioniert und Correct
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederwird abgelehnt, weil x und y nicht denselben Typ haben, was das richtige
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederVerhalten auch im ersten Fall w\x{00E4}re.
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederfor CSP-CASL example: with logic
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederheterogeneous static ana
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maedertheorem links between nodes in different libraries
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaederbasicProofs: use info about used axioms
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder ensure that axiom/thm names are unique
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaederOverload / inlineAxioms: injections
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederremove "prove" menu in abstracted dg
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maederbetter sublogic analysis in codings
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maederthy files in subdir
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederadjust path for thy files, such that hets can also be started from subdirs
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederRestrict Sonjas simplifications to HasCASL
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederadd suitable axioms to simplifier and CR
4fc727afa544a757d1959ce77c02208f8bf330dcChristian MaedercomputeTheory: remove double axioms
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederadd suitable axioms to simplifier and classical reasoner
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maederbetter display of internal nodes (use tooltip?)
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maederupdate Hets, CASL, daVinci on web page
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederCASL2PCFOL: x_i -> t_i, t=[inj(x_i)]
4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maederpacking of binaries: add hets-update, refer to TclTk
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maedertest for sublogic before applying comorphism
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederMissing points for heterogeneous WADT 04 example:
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder- coding to Isabelle: translate sort gen constraints
4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maeder- Improve adapation to Isabelle's lexis
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederIsabelle: (ask Christoph)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder remove datatypes from sort list
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder prove local thm link (=> green)
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder "prove" menu with choice windows
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder incorporate sublogics
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder sublogic translation table
b1caf27fb0c879dd39600d09d501074a2dfd865aChristian Maeder better interaction between Isabelle instance (for one node)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski + selection of single goals that are proved
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder => use PGIP interface (Christoph, David)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder correct show theory
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder Keep proofs and lemmas in .thy files (kind of merge)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski CASL-like syntax
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder CASL annotation for lemmas that should be used in proof
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski inherit CASL's mixfix syntax
5e46b572ed576c0494768998b043d9d340594122Till MossakowskiSignatures versus theories: where to store additional infos?
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskicomp(id,x)=x for comorphism names
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederGeneralise CASL2Modal
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederMixfix analysis + typecheck for modality axiomatizations
5e46b572ed576c0494768998b043d9d340594122Till MossakowskiModal logics: modal logic, temporal logic, mu calculus
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder+ translations (e.g. modal to FOL)
329d1810c6d5a5a0827e1d07503d94431578d176Christian MaederCASL->Haskell with free DTs (mark sortgens) + recursion
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder- List[Dec] wird List[Pos]
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder- George wg. Schlie�en von Fenstern
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder- node numbers do not match
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder- thm links with external target should be provable as well
329d1810c6d5a5a0827e1d07503d94431578d176Christian MaederRemove warnings
329d1810c6d5a5a0827e1d07503d94431578d176Christian MaederDifferent types of logic translations
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederImprove Static analysis of structured specs
329d1810c6d5a5a0827e1d07503d94431578d176Christian MaederDevelopment graph calculus, Strategies for DG rules
329d1810c6d5a5a0827e1d07503d94431578d176Christian MaederManagement of change
329d1810c6d5a5a0827e1d07503d94431578d176Christian MaederIntegrate provers
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder Otter model checker
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski FOL-prover by Uli Furhbach
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Isabelle codings: www.inf.ethz.ch/~vigano
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Renate Schmidt, Manchester: uses FOL prover for description logic
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (as efficient as DL-specific tools!)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Look at PROSPER toolkit
243b39800f5ea9033daca8ce5475531d114e1877Christian Maeder consistency: see IJCAR-workshop on non-provability in Cork
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski IJCAR workshop about logical frameworks and meta-languages
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederKlaus' wayfinding example
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maederask Detlef: critical pairs, Fossacs paper by Francesco
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederUniForM workbench:
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maederfirst steps towards CASL instance, using ATerms and re-using MMISS instance
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maedervariants for specs (needed for DOLCE: CASL variant, DL variant, ...)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederIntegration of MAYA and Isabelle/HOL (global HOL-Coding of
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Grothendieck logic)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder + for TAS: reflection of HOL in HOL, to be composed with encodings
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder (i.e. signatures, axioms, signature morphisms in HOL,
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder re-use ML signatures) (Einar)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederDisplay Specs as daVinci subgraphs
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederUser interface
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder--------------
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederLogic graph window
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederInput text window
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederDevelopment graph window
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederProver windows
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder************************************************
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder************************************************
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederHets 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)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederPackaging of installation
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederGUI (vgl. VSE)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder with Eclipse, WXHaskell or GTk?
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder how to integrate with event system of UniForM workbench?
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maederintegrate graphviz (or use Java interface for racer? or Isabelle browser? or...?)
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder this interacts with GUI!
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederData.Serizable (only when ghc supports it)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maederincrease performance
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maederintegrate QuickCheck: come to lecture!
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder++++++++++++++++++++++++++++++++++++++++++++++++
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederRemaining things
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder++++++++++++++++++++++++++++++++++++++++++++++++
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaederMark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Coq, PTT in Maude
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederProofs with basic datatypes
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederVerbesserung der Fehlermeldungen
746440cc1b984a852f5864235b8fa3930963a081Christian MaederImprove encoding: CATS/basic_encode.sml (3 days)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederMore HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederRenamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederExample of Agnes und Frank: proofs in HOL-CASL (2 days)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederTerm input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederExamples for cond rewriting -> Christophe
746440cc1b984a852f5864235b8fa3930963a081Christian MaederDoku: VSE-Prover, VSE-Method VSE-demo in Bremen?
746440cc1b984a852f5864235b8fa3930963a081Christian MaederAdapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiEigene IsaWin-Instanz mit CASL-RS statt HOL-RS
3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till MossakowskiHOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederHOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederHOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)
3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till MossakowskiEncoding of structured free (3 days)
3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till MossakowskiEncoding of structured cofree (2 weeks)
3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till MossakowskiEingabesyntax als Mix zwischen CASL und HOL (3 days)
3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till MossakowskiAdapt Isabelle unions to CASL unions (1 week)
ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till MossakowskiIsaWin git/src/isa_ext/casl_thy.sml (1 week)
ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till MossakowskiGenerate Proof obligations (1 week)
ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till MossakowskiAdd renaming to Isabelle kernel (2 months)
ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till MossakowskiRepository mit korrekten und fehlerhaften Specs
ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till MossakowskiHetCATS User manual, Doku fuer Environments (2 weeks)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangConversion ASF/SDF-Parser -> abstract syntax (in Haskell)
239fe94380bba365636e6ac48e094fc92cae30c7Christian MaederComparsion of parsers (ML-yacc parser, SDF-Parser)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangConversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederPVS anbinden (Kooperation mit Cachan?)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangPortations: Intel-Solaris, Mac OS-10 (2 weeks)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangViews on CASL specs: CATS/viewer.sml (2 weeks)
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederUebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangModule graph CATS/module_graph.sml (1 week) -> Maya?
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederATerms via XML: CATS/aterms.sml (2 weeks)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangNeues Tool-Schaubild auf Web-Seiten ver�ffentlichen
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiLibrary management: CATS/lib_ana.sml (2 weeks)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangVersion management/Uniform Workbench: CATS/lib_ana.sml (2 months)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski{- This does not work due to needed ordering:
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wanginstance Functor Set where
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang fmap = mapSet
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederinstance Monad Set where
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang return = unitSet
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang m >>= k = unionManySets (setToList (fmap k m))
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangAufbau von comptable