577N/APlan and priority list for CoFI tool activities

577N/A

1339N/Amost things have been moved to the new bug tracking system

577N/A

1409N/Asee http://trac.informatik.uni-bremen.de:8080/hets

577N/A

577N/A************************************************

919N/AKlaus

919N/A************************************************

919N/A

919N/Afor ProofManagement-GUI

919N/A provide structured (based on spec-names) selection/deselection facility

919N/A of axioms and theorems

919N/A

919N/Atrace if liniarity of sentences along development is given

919N/A

919N/AIgnore axiom selection for interactive provers

919N/A

919N/A((

919N/AImprovements:

919N/A * display node name (instead of number) in uDrawGraph widow title

919N/A * add conversion of equivalent sorts into special arrow

919N/A * needs modification of Taxnomy Graph

919N/A

577N/ATranslation between Achim's ontology data structure and CASL (in Hets)

577N/A

577N/Avisualization of "taxonomy" of CASL signatures

577N/A (subsorts = inheritance, unary preds = concepts, binary preds = relations)

577N/A

577N/A last two ... partially done

1370N/A))

577N/A

911N/ARecognize guarded fragment of CASL:

1370N/A G ::= forall x . At(x) => G where At is a conjunction of atoms

1370N/A | exists x . At(x) /\ G

1370N/A

911N/A

577N/ABitte auch aus folgenden Files die todo-Listen nach Trac verschieben:

1370N/A

1409N/ACASL_DL/AS_CASL_DL.der.hs:{- todo:

577N/ACASL_DL/PredefinedGlobalAnnos.hs: todo:

577N/ACASL_DL/PredefinedSign.inline.hs: todo:

577N/ACASL_DL/Sign.hs: todo:

577N/ACASL_DL/StatAna.hs:{- todo:

577N/AComorphisms/CASL2SPASS.hs:{- todo

577N/AComorphisms/KnownProvers.hs:{- todo:

577N/AComorphisms/Modal2CASL.inline.hs: todo:

577N/AOWL_DL/Logic_OWL_DL.hs:{- todo:

1339N/AOWL_DL/Print.hs: todo:

1339N/AOWL_DL/ReadWrite.der.hs:{- todo:

970N/AOWL_DL/ReadWrite.hs:{- todo:

970N/AOWL_DL/StructureAna.hs: -- TODO: check if gEmbed (Logic.Grothendieck) and G_morphism

970N/AGUI/ProofManagement.hs: todo:

970N/AGUI/ProofManagement.hs: -- TODO: do something with the resulting G_theory before returning it?

970N/AGUI/hets_cgi.hs: todo:

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

970N/ASPASS/PrintTPTP.hs:{- todo:

970N/ASPASS/Logic_SPASS.hs: is_subsig SoftFOL = const $ const True -- TODO!!

970N/ATaxonomy/MMiSSOntology.hs: todo: add a new edge type for equivalence which should be visited only once

970N/ACommon/LaTeX_funs.hs: TODO:

970N/ACommon/LaTeX_funs.hs: -- TODO: Build a nice correction map

577N/ALogic/Prover.hs:{- todo:

1072N/A

577N/A************************************************

577N/AChristian

577N/A************************************************

1072N/A

1124N/ABitte auch aus folgenden Files die todo-Listen nach Trac verschieben:

1124N/A

1072N/ADriver/Options.hs:-- | 'Flattening' describes how flat the Earth really is (TODO: add comment)

1072N/AIsabelle/Logic_Isabelle.hs: is_subsig Isabelle = const $ const True -- TODO!!

577N/ACASL/Morphism.hs:todo:

577N/AIsabelle/IsaPrint.hs: todo: brackets in (? x . p x) ==> q

577N/AIsabelle/IsaProve.hs: todo: thy files in subdir, check of legal changes in thy file

615N/A

615N/A************************************************

615N/ATill

1196N/A************************************************

1196N/A

1196N/ABitte auch aus folgenden Files die todo-Listen nach Trac verschieben:

1196N/A

1196N/AProofs/Automatic.hs:todo in general:

1196N/AProofs/Automatic.hs:{- todo: implement apply for GlobDecomp and Subsumption

810N/AProofs/EdgeUtils.hs:{- todo: also treat conservativity proof status in computation of proof basis

1097N/AProofs/EdgeUtils.hs: _ -> Right False -- todo: also treat conservativity proof status

935N/AProofs/Global.hs:todo for Jorina:

810N/AProofs/HideTheoremShift.hs: todo: use compInclusion instead of compHomInclusion

970N/AProofs/InferBasic.hs:todo:

970N/AStatic/AnalysisArchitecture.hs:{- todo:

970N/AStatic/DevGraph.hs:todo:

577N/ASyntax/Parse_AS_Structured.hs: todo:

577N/ACASL/Amalgamability.hs:TODO:

577N/ACASL/Amalgamability.hs: -- TODO: generate proof obligations

1072N/AProofs/InferBasic.hs: -- TODO: Reimplement stuff

1097N/AStatic/DevGraph.hs: dgl_type = GlobalDef, -- TODO: other type

970N/AStatic/DevGraph.hs: dgl_type = GlobalDef, -- TODO: other type

577N/AStatic/LogicStructured.hs: TODO

1072N/AStatic/LogicStructured.hs:-- see TODO section for possible extensions for (isJust enc) and

1097N/ASyntax/Parse_AS_Architecture.hs: TODO:

1072N/ASyntax/Parse_AS_Library.hs: TODO:

577N/A

970N/Aan Hiwis delegiert:

970N/AConstraintCASL/Logic_ConstraintCASL.hs:{- todo:

ConstraintCASL/StaticAna.hs:{- todo: check formulas -}

OMDoc/OMDocOutput.hs: BUGS/TODO:

OMDoc/Util.hs:-- TODO : this looks very slow...

PGIP/Utils.hs:{- todo: refactor getGoalList, extractGraphEdge, extractGraphLabeledEdge

PGIP/Command_Parser.hs: TODO :

PGIP/Commands.hs: TODO :

CspCASL/Logic_CspCASL.hs: todo:

CspCASL/SignCSP.hs:-- todo: implement isInclusion, computeExt

CspCASL/StatAnaCSP.hs:{- todo: