todo revision 7c610eb832a4575b209fc6e6c674b99975135012
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:
GUI/ProofManagement.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:
Taxonomy/MMiSSOntology.hs: todo: add a new edge type for equivalence which should be visited only once
************************************************
Christian
************************************************
Bitte auch aus folgenden Files die todo-Listen nach Trac verschieben:
Comorphisms/CoCFOL2IsabelleHOL.hs:{- todo:
HasCASL/Sublogic.hs:{- todo: test computations
CASL/Sublogic.hs:-- to do: implement pr_sign
************************************************
Till
************************************************
Bitte auch aus folgenden Files die todo-Listen nach Trac verschieben:
CASL/Morphism.hs:todo:
CoCASL/Logic_CoCASL.hs:{- todo:
CoCASL/StatAna.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/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: