144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPlan and priority list for CoFI tool activities

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

4b90c3b8ee582daeead21ce272f11c952ef1631eTill Mossakowskimost things have been moved to the new bug tracking system

cc9279b89cc62b80199696ac7e87b6d2bdd08e7aTill Mossakowski

5f40e8aa2c372040ab519c6401627d64812922ffKlaus Luettichsee http://trac.informatik.uni-bremen.de:8080/hets

c1015e823b467ffb3e58fe3eacb0db58937063baTill Mossakowski

baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************

baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichKlaus

baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************

aa6f6fa09091e92016598584162b9ba909af48ccTill Mossakowski

ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettichfor ProofManagement-GUI

ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich provide structured (based on spec-names) selection/deselection facility

ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich of axioms and theorems

ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich

ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettichtrace if liniarity of sentences along development is given

ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich

e0eee2b8144337bb54feb78d5a8b043041c9e028Till MossakowskiIgnore axiom selection for interactive provers

e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski

89ee5859757b78fefccda0a582cc896bd422d006Klaus Luettich((

89ee5859757b78fefccda0a582cc896bd422d006Klaus LuettichImprovements:

89ee5859757b78fefccda0a582cc896bd422d006Klaus Luettich * display node name (instead of number) in uDrawGraph widow title

89ee5859757b78fefccda0a582cc896bd422d006Klaus Luettich * add conversion of equivalent sorts into special arrow

89ee5859757b78fefccda0a582cc896bd422d006Klaus Luettich * needs modification of Taxnomy Graph

89ee5859757b78fefccda0a582cc896bd422d006Klaus Luettich

b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiTranslation between Achim's ontology data structure and CASL (in Hets)

b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskivisualization of "taxonomy" of CASL signatures

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (subsorts = inheritance, unary preds = concepts, binary preds = relations)

baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich

baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich last two ... partially done

89ee5859757b78fefccda0a582cc896bd422d006Klaus Luettich))

baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRecognize guarded fragment of CASL:

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski G ::= forall x . At(x) => G where At is a conjunction of atoms

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski | exists x . At(x) /\ G

baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiBitte auch aus folgenden Files die todo-Listen nach Trac verschieben:

7c610eb832a4575b209fc6e6c674b99975135012Till Mossakowski

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiCASL_DL/AS_CASL_DL.der.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiCASL_DL/PredefinedGlobalAnnos.hs: todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiCASL_DL/PredefinedSign.inline.hs: todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiCASL_DL/Sign.hs: todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiCASL_DL/StatAna.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiComorphisms/CASL2SPASS.hs:{- todo

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiComorphisms/KnownProvers.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiComorphisms/Modal2CASL.inline.hs: todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiOWL_DL/Logic_OWL_DL.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiOWL_DL/Print.hs: todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiOWL_DL/ReadWrite.der.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiOWL_DL/ReadWrite.hs:{- todo:

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill MossakowskiOWL_DL/StructureAna.hs: -- TODO: check if gEmbed (Logic.Grothendieck) and G_morphism

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiGUI/ProofManagement.hs: todo:

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill MossakowskiGUI/ProofManagement.hs: -- TODO: do something with the resulting G_theory before returning it?

5ee17de4af53fad27df89dd51a92c599a6fcd75eTill MossakowskiGUI/hets_cgi.hs: todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiSPASS/DFGParser.hs:quantification s = do (ts',t') <- parens (do ts <- squares (commaSep1 term) -- todo: var binding should allow only simple terms

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiSPASS/PrintTPTP.hs:{- todo:

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill MossakowskiSPASS/Logic_SPASS.hs: is_subsig SoftFOL = const $ const True -- TODO!!

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiTaxonomy/MMiSSOntology.hs: todo: add a new edge type for equivalence which should be visited only once

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill MossakowskiCommon/LaTeX_funs.hs: TODO:

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill MossakowskiCommon/LaTeX_funs.hs: -- TODO: Build a nice correction map

5ee17de4af53fad27df89dd51a92c599a6fcd75eTill MossakowskiLogic/Prover.hs:{- todo:

ca4a7ebff140096ece1bb67b46fbecfb9305feecTill MossakowskiCommon/Utils.hs: Todo:

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill Mossakowski

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill Mossakowski************************************************

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill MossakowskiChristian

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill Mossakowski************************************************

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill Mossakowski

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill MossakowskiBitte auch aus folgenden Files die todo-Listen nach Trac verschieben:

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill Mossakowski

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill MossakowskiDriver/Options.hs:-- | 'Flattening' describes how flat the Earth really is (TODO: add comment)

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill MossakowskiIsabelle/Logic_Isabelle.hs: is_subsig Isabelle = const $ const True -- TODO!!

5ee17de4af53fad27df89dd51a92c599a6fcd75eTill MossakowskiCASL/Morphism.hs:todo:

5ee17de4af53fad27df89dd51a92c599a6fcd75eTill MossakowskiIsabelle/IsaPrint.hs: todo: brackets in (? x . p x) ==> q

5ee17de4af53fad27df89dd51a92c599a6fcd75eTill MossakowskiIsabelle/IsaProve.hs: todo: thy files in subdir, check of legal changes in thy file

7c610eb832a4575b209fc6e6c674b99975135012Till Mossakowski

7c610eb832a4575b209fc6e6c674b99975135012Till Mossakowski************************************************

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiTill

7c610eb832a4575b209fc6e6c674b99975135012Till Mossakowski************************************************

7c610eb832a4575b209fc6e6c674b99975135012Till Mossakowski

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiBitte auch aus folgenden Files die todo-Listen nach Trac verschieben:

7c610eb832a4575b209fc6e6c674b99975135012Till Mossakowski

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiProofs/EdgeUtils.hs:{- todo: also treat conservativity proof status in computation of proof basis

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiProofs/EdgeUtils.hs: _ -> Right False -- todo: also treat conservativity proof status

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiProofs/Global.hs:todo for Jorina:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiProofs/HideTheoremShift.hs: todo: use compInclusion instead of compHomInclusion

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiProofs/InferBasic.hs:todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiStatic/AnalysisArchitecture.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiStatic/DevGraph.hs:todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiSyntax/Parse_AS_Structured.hs: todo:

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill MossakowskiCASL/Amalgamability.hs:TODO:

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill MossakowskiCASL/Amalgamability.hs: -- TODO: generate proof obligations

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill MossakowskiProofs/InferBasic.hs: -- TODO: Reimplement stuff

ca4a7ebff140096ece1bb67b46fbecfb9305feecTill MossakowskiLogic/Comorphism.hs: Todo:

ca4a7ebff140096ece1bb67b46fbecfb9305feecTill MossakowskiLogic/Morphism.hs: Todo:

ca4a7ebff140096ece1bb67b46fbecfb9305feecTill MossakowskiStatic/AnalysisLibrary.hs: Todo:

ca4a7ebff140096ece1bb67b46fbecfb9305feecTill MossakowskiStatic/AnalysisStructured.hs: Todo:

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill MossakowskiStatic/DevGraph.hs: dgl_type = GlobalDef, -- TODO: other type

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill MossakowskiStatic/DevGraph.hs: dgl_type = GlobalDef, -- TODO: other type

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill MossakowskiStatic/LogicStructured.hs: TODO

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill MossakowskiStatic/LogicStructured.hs:-- see TODO section for possible extensions for (isJust enc) and

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill MossakowskiSyntax/Parse_AS_Architecture.hs: TODO:

183e25edd6aaf48da3cfcf6e5a5300bed5a941dfTill MossakowskiSyntax/Parse_AS_Library.hs: TODO:

ca4a7ebff140096ece1bb67b46fbecfb9305feecTill MossakowskiCoCASL/Sublogic.hs:-- Todo: add projection functions when those for CASL are settled

5ee17de4af53fad27df89dd51a92c599a6fcd75eTill Mossakowski

5ee17de4af53fad27df89dd51a92c599a6fcd75eTill Mossakowskian Hiwis delegiert:

5ee17de4af53fad27df89dd51a92c599a6fcd75eTill MossakowskiConstraintCASL/Logic_ConstraintCASL.hs:{- todo:

5ee17de4af53fad27df89dd51a92c599a6fcd75eTill MossakowskiConstraintCASL/StaticAna.hs:{- todo: check formulas -}

5ee17de4af53fad27df89dd51a92c599a6fcd75eTill MossakowskiOMDoc/OMDocOutput.hs: BUGS/TODO:

5ee17de4af53fad27df89dd51a92c599a6fcd75eTill MossakowskiOMDoc/Util.hs:-- TODO : this looks very slow...

5ee17de4af53fad27df89dd51a92c599a6fcd75eTill MossakowskiPGIP/Utils.hs:{- todo: refactor getGoalList, extractGraphEdge, extractGraphLabeledEdge

5ee17de4af53fad27df89dd51a92c599a6fcd75eTill MossakowskiPGIP/Command_Parser.hs: TODO :

5ee17de4af53fad27df89dd51a92c599a6fcd75eTill MossakowskiPGIP/Commands.hs: TODO :

5ee17de4af53fad27df89dd51a92c599a6fcd75eTill Mossakowski

5ee17de4af53fad27df89dd51a92c599a6fcd75eTill MossakowskiCspCASL/Logic_CspCASL.hs: todo:

5ee17de4af53fad27df89dd51a92c599a6fcd75eTill MossakowskiCspCASL/SignCSP.hs:-- todo: implement isInclusion, computeExt

5ee17de4af53fad27df89dd51a92c599a6fcd75eTill MossakowskiCspCASL/StatAnaCSP.hs:{- todo:

ca4a7ebff140096ece1bb67b46fbecfb9305feecTill Mossakowski

ca4a7ebff140096ece1bb67b46fbecfb9305feecTill Mossakowski