todo revision 5cfeedad8c9d43f62f8e8b85ab73c0dd4e91d976
Plan and priority list for CoFI tool activities
most things have been moved to the new bug tracking system
************************************************
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/Sign.hs: todo:
CASL_DL/StatAna.hs:{- todo:
Comorphisms/CASL2SPASS.hs:{- todo
Comorphisms/KnownProvers.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?
GUI/hets_cgi.hs: todo:
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
Logic/Prover.hs:{- todo:
Common/Utils.hs: Todo:
************************************************
Christian
************************************************
************************************************
Till
************************************************
Bitte auch aus folgenden Files die todo-Listen nach Trac verschieben:
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:
CASL/Amalgamability.hs:TODO:
CASL/Amalgamability.hs: -- TODO: generate proof obligations
Proofs/InferBasic.hs: -- TODO: Reimplement stuff
Logic/Comorphism.hs: Todo:
Logic/Morphism.hs: Todo:
Static/AnalysisLibrary.hs: Todo:
Static/AnalysisStructured.hs: Todo:
Static/DevGraph.hs: dgl_type = GlobalDef, -- TODO: other type
Static/DevGraph.hs: dgl_type = GlobalDef, -- TODO: other type
Static/LogicStructured.hs:-- see TODO section for possible extensions for (isJust enc) and
Syntax/Parse_AS_Library.hs: TODO:
CoCASL/Sublogic.hs:-- Todo: add projection functions when those for CASL are settled
an Hiwis delegiert:
ConstraintCASL/StaticAna.hs:{- todo: check formulas -}
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: