Plan and priority list for CoFI tool activities

most things have been moved to the new bug tracking system

see http://trac.informatik.uni-bremen.de:8080/hets

************************************************

Klaus

************************************************

for ProofManagement-GUI

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

of axioms and theorems

trace if liniarity of sentences along development is given

Ignore axiom selection for interactive provers

((

Improvements:

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

* add conversion of equivalent sorts into special arrow

* needs modification of Taxnomy Graph

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

visualization of "taxonomy" of CASL signatures

(subsorts = inheritance, unary preds = concepts, binary preds = relations)

last two ... partially done

))

Recognize guarded fragment of CASL:

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

| exists x . At(x) /\ G

Bitte auch aus folgenden Files die todo-Listen nach Trac verschieben:

CASL_DL/AS_CASL_DL.der.hs:{- todo:

CASL_DL/PredefinedGlobalAnnos.hs: todo:

CASL_DL/PredefinedSign.inline.hs: todo:

CASL_DL/Sign.hs: todo:

CASL_DL/StatAna.hs:{- todo:

Comorphisms/CASL2SPASS.hs:{- todo

Comorphisms/KnownProvers.hs:{- todo:

Comorphisms/Modal2CASL.inline.hs: todo:

OWL_DL/Logic_OWL_DL.hs:{- todo:

OWL_DL/Print.hs: todo:

OWL_DL/ReadWrite.der.hs:{- todo:

OWL_DL/ReadWrite.hs:{- todo:

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

GUI/ProofManagement.hs: todo:

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

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

SPASS/PrintTPTP.hs:{- todo:

SPASS/Logic_SPASS.hs: is_subsig SoftFOL = const $ const True -- TODO!!

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

Common/LaTeX_funs.hs: TODO:

Common/LaTeX_funs.hs: -- TODO: Build a nice correction map

************************************************

Christian

************************************************

Bitte auch aus folgenden Files die todo-Listen nach Trac verschieben:

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

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

************************************************

Till

************************************************

Bitte auch aus folgenden Files die todo-Listen nach Trac verschieben:

CASL/Morphism.hs:todo:

CASL/SymbolMapAnalysis.hs:todo:

CoCASL/Logic_CoCASL.hs:{- todo:

CoCASL/StatAna.hs:{- todo:

ConstraintCASL/Logic_ConstraintCASL.hs:{- todo:

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

CspCASL/Logic_CspCASL.hs: todo:

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

CspCASL/StatAnaCSP.hs:{- todo:

GUI/ConvertDevToAbstractGraph.hs: todo:

GUI/hets_cgi.hs: todo:

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

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

Logic/Grothendieck.hs:{- todo: somthing like the following...

Logic/Prover.hs:{- todo:

Modal/Logic_Modal.hs:{- todo:

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

Proofs/Automatic.hs:todo in general:

Proofs/Automatic.hs:{- todo: implement apply for GlobDecomp and Subsumption

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

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

Proofs/Global.hs:todo for Jorina:

Proofs/HideTheoremShift.hs: todo: use compInclusion instead of compHomInclusion

Proofs/InferBasic.hs:todo:

Static/AnalysisArchitecture.hs:{- todo:

Static/DevGraph.hs:todo:

Syntax/Parse_AS_Structured.hs: todo:

CASL/Amalgamability.hs:TODO:

CASL/Amalgamability.hs: -- TODO: generate proof obligations

OMDoc/OMDocOutput.hs: BUGS/TODO:

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

PGIP/Command_Parser.hs: TODO :

PGIP/Commands.hs: TODO :

Proofs/InferBasic.hs: -- TODO: Reimplement stuff

Static/DevGraph.hs: dgl_type = GlobalDef, -- TODO: other type

Static/DevGraph.hs: dgl_type = GlobalDef, -- TODO: other type

Static/LogicStructured.hs: TODO

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

Syntax/Parse_AS_Architecture.hs: TODO:

Syntax/Parse_AS_Library.hs: TODO: